mathlib documentation

data.equiv.encodable.basic

@[class]
structure encodable (α : Type u_1) :
Type u_1

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

Instances
def encodable.of_left_injection {α : Type u_1} {β : Type u_2} [encodable α] (f : β → α) (finv : α → option β) (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 : ) :
@[instance]
Equations
@[simp]
@[simp]
@[instance]
Equations
@[instance]
Equations
@[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 α] :
@[simp]
def encodable.decode2 (α : Type u_1) [encodable α] (n : ) :
Equations
theorem encodable.mem_decode2' {α : Type u_1} [encodable α] {n : } {a : α} :
theorem encodable.mem_decode2 {α : Type u_1} [encodable α] {n : } {a : α} :
theorem encodable.decode2_inj {α : Type u_1} [encodable α] {n : } {a₁ a₂ : α} (h₁ : a₁ encodable.decode2 α n) (h₂ : a₂ encodable.decode2 α n) :
a₁ = a₂
theorem encodable.encodek2 {α : Type u_1} [encodable α] (a : α) :
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
@[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 : ) :
def encodable.encode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :
sigma γ
Equations
def encodable.decode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ) :
Equations
@[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 : ) :
@[simp]
theorem encodable.encode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (a : α) (b : γ a) :
@[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 : ) :
@[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
@[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) :
@[instance]
def encodable.fin (n : ) :
Equations
@[instance]
def encodable.ulift {α : Type u_1} [encodable α] :
Equations
@[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
@[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
@[instance]
def ulower.encodable (α : Type u_1) [encodable α] :
def ulower.equiv (α : Type u_1) [encodable α] :
α ulower α

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
@[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 α} :
@[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 : α} :
@[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 α] [decidable_pred p] (h : ∃ (x : α), p x) :
{a // p a}
Equations
def encodable.choose {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :
α
Equations
theorem encodable.choose_spec {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :
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
def directed.sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} (f : α → β) (hf : directed r 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
theorem directed.sequence_mono_nat {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} {f : α → β} (hf : directed r f) (n : ) :
r (f (directed.sequence f hf n)) (f (directed.sequence f hf (n + 1)))
theorem directed.rel_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} {f : α → β} (hf : directed r f) (a : α) :
r (f a) (f (directed.sequence f hf (encodable.encode a + 1)))
theorem directed.sequence_mono {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : directed has_le.le f) :
theorem directed.le_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : directed has_le.le f) (a : α) :
def quotient.rep {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [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 α} [decidable_rel has_equiv.equiv] [encodable α] (q : quotient s) :

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

Equations