# mathlibdocumentation

data.equiv.encodable.basic

@[class]
structure encodable (α : Type u_1) :
Type u_1
• encode : α →
• decode :
• encodek : ∀ (a : α),

An encodable type is a "constructively countable" type. This is where we have an explicit injection encode : α → nat and a partial inverse decode : nat → option α. This makes the range of encode decidable, although it is not decidable if α is finite or not.

Instances
theorem encodable.encode_injective {α : Type u_1} [encodable α] :
theorem encodable.surjective_decode_iget (α : Type u_1) [encodable α] [inhabited α] :
def encodable.decidable_eq_of_encodable (α : Type u_1) [encodable α] :
Equations
def encodable.of_left_injection {α : Type u_1} {β : Type u_2} [encodable α] (f : β → α) (finv : α → ) (linv : ∀ (b : β), finv (f b) = some b) :
Equations
def encodable.of_left_inverse {α : Type u_1} {β : Type u_2} [encodable α] (f : β → α) (finv : α → β) (linv : ∀ (b : β), finv (f b) = b) :
Equations
def encodable.of_equiv {β : Type u_2} (α : Type u_1) [encodable α] (e : β α) :

If α is encodable and β ≃ α, then so is β

Equations
• = _
@[simp]
theorem encodable.encode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β α) (b : β) :
@[simp]
theorem encodable.decode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β α) (n : ) :
@[protected, instance]
Equations
@[simp]
theorem encodable.encode_nat (n : ) :
@[simp]
theorem encodable.decode_nat (n : ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem encodable.encode_star  :
@[simp]
@[simp]
theorem encodable.decode_unit_succ (n : ) :
@[protected, instance]
def encodable.option {α : Type u_1} [h : encodable α] :
Equations
@[simp]
theorem encodable.encode_none {α : Type u_1} [encodable α] :
@[simp]
theorem encodable.encode_some {α : Type u_1} [encodable α] (a : α) :
@[simp]
theorem encodable.decode_option_zero {α : Type u_1} [encodable α] :
0 =
@[simp]
theorem encodable.decode_option_succ {α : Type u_1} [encodable α] (n : ) :
n.succ =
def encodable.decode2 (α : Type u_1) [encodable α] (n : ) :
Equations
theorem encodable.mem_decode2' {α : Type u_1} [encodable α] {n : } {a : α} :
a a
theorem encodable.mem_decode2 {α : Type u_1} [encodable α] {n : } {a : α} :
a
theorem encodable.decode2_is_partial_inv {α : Type u_1} [encodable α] :
theorem encodable.decode2_inj {α : Type u_1} [encodable α] {n : } {a₁ a₂ : α} (h₁ : a₁ ) (h₂ : a₂ ) :
a₁ = a₂
theorem encodable.encodek2 {α : Type u_1} [encodable α] (a : α) :
def encodable.decidable_range_encode (α : Type u_1) [encodable α] :
Equations
def encodable.equiv_range_encode (α : Type u_1) [encodable α] :
Equations
def encodable.encode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
α β
Equations
def encodable.decode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
option β)
Equations
• = encodable.decode_sum._match_1 n.bodd_div2
• encodable.decode_sum._match_1 (tt, m) =
• encodable.decode_sum._match_1 (ff, m) =
@[protected, instance]
def encodable.sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
encodable β)
Equations
@[simp]
theorem encodable.encode_inl {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) :
@[simp]
theorem encodable.encode_inr {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (b : β) :
@[simp]
theorem encodable.decode_sum_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
@[protected, instance]
Equations
@[simp]
theorem encodable.encode_tt  :
@[simp]
theorem encodable.encode_ff  :
@[simp]
theorem encodable.decode_zero  :
@[simp]
theorem encodable.decode_one  :
theorem encodable.decode_ge_two (n : ) (h : 2 n) :
def encodable.encode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :
Equations
def encodable.decode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ) :
Equations
• = encodable.decode_sigma._match_1 n.unpair
• encodable.decode_sigma._match_1 (n₁, n₂) = n₁).bind (λ (a : α), (encodable.decode (γ a) n₂))
@[protected, instance]
def encodable.sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :
Equations
@[simp]
theorem encodable.decode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ) :
n = n.unpair.fst).bind (λ (a : α), (encodable.decode (γ a) n.unpair.snd))
@[simp]
theorem encodable.encode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (a : α) (b : γ a) :
@[protected, instance]
def encodable.prod {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
encodable × β)
Equations
@[simp]
theorem encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
encodable.decode × β) n = n.unpair.fst).bind (λ (a : α), n.unpair.snd))
@[simp]
theorem encodable.encode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) (b : β) :
def encodable.encode_subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] :
{a // P a}
Equations
def encodable.decode_subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] (v : ) :
option {a // P a}
Equations
@[protected, instance]
def encodable.subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] :
encodable {a // P a}
Equations
theorem encodable.subtype.encode_eq {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] (a : subtype P) :
@[protected, instance]
def encodable.fin (n : ) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def encodable.ulift {α : Type u_1} [encodable α] :
Equations
@[protected, instance]
def encodable.plift {α : Type u_1} [encodable α] :
Equations
def encodable.of_inj {α : Type u_1} {β : Type u_2} [encodable β] (f : α → β) (hf : function.injective f) :
Equations
@[protected, instance]
def ulower.decidable_eq (α : Type u_1) [encodable α] :
def ulower (α : Type u_1) [encodable α] :
Type

ulower α : Type 0 is an equivalent type in the lowest universe, given encodable α.

Equations
@[protected, instance]
def ulower.encodable (α : Type u_1) [encodable α] :
def ulower.equiv (α : Type u_1) [encodable α] :
α

The equivalence between the encodable type α and ulower α : Type 0.

Equations
def ulower.down {α : Type u_1} [encodable α] (a : α) :

Lowers an a : α into ulower α.

Equations
@[protected, instance]
def ulower.inhabited {α : Type u_1} [encodable α] [inhabited α] :
Equations
def ulower.up {α : Type u_1} [encodable α] (a : ulower α) :
α

Lifts an a : ulower α into α.

Equations
@[simp]
theorem ulower.down_up {α : Type u_1} [encodable α] {a : ulower α} :
= a
@[simp]
theorem ulower.up_down {α : Type u_1} [encodable α] {a : α} :
@[simp]
theorem ulower.up_eq_up {α : Type u_1} [encodable α] {a b : ulower α} :
a.up = b.up a = b
@[simp]
theorem ulower.down_eq_down {α : Type u_1} [encodable α] {a b : α} :
a = b
@[protected, ext]
theorem ulower.ext {α : Type u_1} [encodable α] {a b : ulower α} :
a.up = b.upa = b
def encodable.choose_x {α : Type u_1} {p : α → Prop} [encodable α] (h : ∃ (x : α), p x) :
{a // p a}
Equations
def encodable.choose {α : Type u_1} {p : α → Prop} [encodable α] (h : ∃ (x : α), p x) :
α
Equations
theorem encodable.choose_spec {α : Type u_1} {p : α → Prop} [encodable α] (h : ∃ (x : α), p x) :
p
theorem encodable.axiom_of_choice {α : Type u_1} {β : α → Type u_2} {R : Π (x : α), β x → Prop} [Π (a : α), encodable (β a)] [Π (x : α) (y : β x), decidable (R x y)] (H : ∀ (x : α), ∃ (y : β x), R x y) :
∃ (f : Π (a : α), β a), ∀ (x : α), R x (f x)
theorem encodable.skolem {α : Type u_1} {β : α → Type u_2} {P : Π (x : α), β x → Prop} [c : Π (a : α), encodable (β a)] [d : Π (x : α) (y : β x), decidable (P x y)] :
(∀ (x : α), ∃ (y : β x), P x y) ∃ (f : Π (a : α), β a), ∀ (x : α), P x (f x)
def encodable.encode' (α : Type u_1) [encodable α] :
α

The encode function, viewed as an embedding.

Equations
@[protected, instance]
def encodable.order.preimage.is_trans {α : Type u_1} [encodable α] :
@[protected, instance]
def encodable.order.preimage.is_antisymm {α : Type u_1} [encodable α] :
@[protected, instance]
def encodable.order.preimage.is_total {α : Type u_1} [encodable α] :
@[protected]
def directed.sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} (f : α → β) (hf : f) :
→ α

Given a directed r function f : α → β defined on an encodable inhabited type, construct a noncomputable sequence such that r (f (x n)) (f (x (n + 1))) and r (f a) (f (x (encode a + 1)).

Equations
• (n + 1) = let p : α := n in directed.sequence._match_1 f hf p n)
• 0 =
• directed.sequence._match_1 f hf p (some a) =
• directed.sequence._match_1 f hf p none =
theorem directed.sequence_mono_nat {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} {f : α → β} (hf : f) (n : ) :
r (f hf n)) (f hf (n + 1)))
theorem directed.rel_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} {f : α → β} (hf : f) (a : α) :
r (f a) (f hf + 1)))
theorem directed.sequence_mono {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : f) :
monotone (f hf)
theorem directed.le_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : f) (a : α) :
f a f hf + 1))
def quotient.rep {α : Type u_1} {s : setoid α} [encodable α] (q : quotient s) :
α

Representative of an equivalence class. This is a computable version of quot.out for a setoid on an encodable type.

Equations
theorem quotient.rep_spec {α : Type u_1} {s : setoid α} [encodable α] (q : quotient s) :
def encodable_quotient {α : Type u_1} {s : setoid α} [encodable α] :

The quotient of an encodable space by a decidable equivalence relation is encodable.

Equations