mathlib documentation

data.equiv.encodable.basic

@[class]
structure encodable  :
Type u_1Type 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 β) :
(∀ (b : β), finv (f b) = some b)encodable β

Equations
def encodable.of_left_inverse {α : Type u_1} {β : Type u_2} [encodable α] (f : β → α) (finv : α → β) :
(∀ (b : β), finv (f b) = b)encodable β

Equations
def encodable.of_equiv {β : Type u_2} (α : Type u_1) [encodable α] :
β αencodable β

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 α] :
option α

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₂ : α} :
a₁ encodable.decode2 α na₂ encodable.decode2 α na₁ = 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 β] :
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)] :
σ γ

Equations
def encodable.decode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :
option (σ γ)

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] :
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 : α → β) :

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 α] :
α → ulower α

Lowers an a : α into ulower α.

Equations
@[instance]
def ulower.inhabited {α : Type u_1} [encodable α] [inhabited α] :

Equations
def ulower.up {α : Type u_1} [encodable α] :
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] :
(∃ (x : α), p x){a // p a}

Equations
def encodable.choose {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] :
(∃ (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)] :
(∀ (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
@[instance]

@[instance]

@[instance]

def directed.sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β → β → Prop} (f : α → β) :
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 α] :
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