mathlib documentation

data.equiv.encodable.basic

@[class]

structure encodable (α : Type u_1) :

Type u_1

encode : α → ℕ
decode : ℕ → option α
encodek : ∀ (a : α), encodable.decode α (encodable.encode a) = some 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 α] :

function.injective encodable.encode

theorem encodable.surjective_decode_iget (α : Type u_1) [encodable α] [inhabited α] :

function.surjective (λ (n : ℕ), (encodable.decode α n).iget)

def encodable.decidable_eq_of_encodable (α : Type u_1) [encodable α] :

decidable_eq α

Equations

encodable.decidable_eq_of_encodable α a b = decidable_of_iff (encodable.encode a = encodable.encode b) _

def encodable.of_left_injection {α : Type u_1} {β : Type u_2} [encodable α] (f : β → α) (finv : α → option β) (linv : ∀ (b : β), finv (f b) = some b) :

Equations

encodable.of_left_injection f finv linv = {encode := λ (b : β), encodable.encode (f b), decode := λ (n : ℕ), (encodable.decode α n).bind finv, encodek := _}

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

Equations

encodable.of_left_inverse f finv linv = encodable.of_left_injection f (some ∘ finv) _

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

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

Equations

encodable.of_equiv α e = encodable.of_left_inverse ⇑e ⇑(e.symm) _

@[simp]

theorem encodable.encode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β ≃ α) (b : β) :

encodable.encode b = encodable.encode (⇑e b)

@[simp]

theorem encodable.decode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β ≃ α) (n : ℕ) :

encodable.decode β n = option.map ⇑(e.symm) (encodable.decode α n)

@[protected, instance]

def encodable.nat :

Equations

encodable.nat = {encode := id ℕ, decode := some ℕ, encodek := encodable.nat._proof_1}

@[simp]

theorem encodable.encode_nat (n : ℕ) :

encodable.encode n = n

@[simp]

theorem encodable.decode_nat (n : ℕ) :

encodable.decode ℕ n = some n

@[protected, instance]

def encodable.empty :

encodable empty

Equations

encodable.empty = {encode := λ (a : empty), empty.rec (λ (a : empty), ℕ) a, decode := λ (n : ℕ), none, encodek := encodable.empty._proof_1}

@[protected, instance]

def encodable.unit :

encodable punit

Equations

encodable.unit = {encode := λ (_x : punit), 0, decode := λ (n : ℕ), n.cases_on (some punit.star) (λ (_x : ℕ), none), encodek := encodable.unit._proof_1}

@[simp]

theorem encodable.encode_star :

encodable.encode punit.star = 0

@[simp]

theorem encodable.decode_unit_zero :

encodable.decode punit 0 = some punit.star

@[simp]

theorem encodable.decode_unit_succ (n : ℕ) :

encodable.decode punit n.succ = none

@[protected, instance]

def encodable.option {α : Type u_1} [h : encodable α] :

encodable (option α)

Equations

encodable.option = {encode := λ (o : option α), o.cases_on 0 (λ (a : α), (encodable.encode a).succ), decode := λ (n : ℕ), n.cases_on (some none) (λ (m : ℕ), option.map some (encodable.decode α m)), encodek := _}

@[simp]

theorem encodable.encode_none {α : Type u_1} [encodable α] :

encodable.encode none = 0

@[simp]

theorem encodable.encode_some {α : Type u_1} [encodable α] (a : α) :

encodable.encode (some a) = (encodable.encode a).succ

@[simp]

theorem encodable.decode_option_zero {α : Type u_1} [encodable α] :

encodable.decode (option α) 0 = some none

@[simp]

theorem encodable.decode_option_succ {α : Type u_1} [encodable α] (n : ℕ) :

encodable.decode (option α) n.succ = option.map some (encodable.decode α n)

def encodable.decode2 (α : Type u_1) [encodable α] (n : ℕ) :

Equations

encodable.decode2 α n = (encodable.decode α n).bind (option.guard (λ (a : α), encodable.encode a = n))

theorem encodable.mem_decode2' {α : Type u_1} [encodable α] {n : ℕ} {a : α} :

a ∈ encodable.decode2 α n ↔ a ∈ encodable.decode α n ∧ encodable.encode a = n

theorem encodable.mem_decode2 {α : Type u_1} [encodable α] {n : ℕ} {a : α} :

a ∈ encodable.decode2 α n ↔ encodable.encode a = n

theorem encodable.decode2_is_partial_inv {α : Type u_1} [encodable α] :

function.is_partial_inv encodable.encode (encodable.decode2 α)

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 : α) :

encodable.decode2 α (encodable.encode a) = some a

def encodable.decidable_range_encode (α : Type u_1) [encodable α] :

decidable_pred (set.range encodable.encode)

Equations

encodable.decidable_range_encode α = λ (x : ℕ), decidable_of_iff ↥((encodable.decode2 α x).is_some) _

def encodable.equiv_range_encode (α : Type u_1) [encodable α] :

α ≃ ↥(set.range encodable.encode)

Equations

encodable.equiv_range_encode α = {to_fun := λ (a : α), ⟨encodable.encode a, _⟩, inv_fun := λ (n : ↥(set.range encodable.encode)), option.get _, left_inv := _, right_inv := _}

def encodable.encode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :

α ⊕ β → ℕ

Equations

encodable.encode_sum (sum.inr b) = bit1 (encodable.encode b)
encodable.encode_sum (sum.inl a) = bit0 (encodable.encode a)

def encodable.decode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ℕ) :

option (α ⊕ β)

Equations

encodable.decode_sum n = encodable.decode_sum._match_1 n.bodd_div2
encodable.decode_sum._match_1 (tt, m) = option.map sum.inr (encodable.decode β m)
encodable.decode_sum._match_1 (ff, m) = option.map sum.inl (encodable.decode α m)

@[protected, instance]

def encodable.sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :

encodable (α ⊕ β)

Equations

encodable.sum = {encode := encodable.encode_sum _inst_2, decode := encodable.decode_sum _inst_2, encodek := _}

@[simp]

theorem encodable.encode_inl {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) :

encodable.encode (sum.inl a) = bit0 (encodable.encode a)

@[simp]

theorem encodable.encode_inr {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (b : β) :

encodable.encode (sum.inr b) = bit1 (encodable.encode b)

@[simp]

theorem encodable.decode_sum_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ℕ) :

encodable.decode (α ⊕ β) n = encodable.decode_sum n

@[protected, instance]

def encodable.bool :

Equations

encodable.bool = encodable.of_equiv (unit ⊕ unit) equiv.bool_equiv_punit_sum_punit

@[simp]

theorem encodable.encode_tt :

encodable.encode tt = 1

@[simp]

theorem encodable.encode_ff :

encodable.encode ff = 0

@[simp]

theorem encodable.decode_zero :

encodable.decode bool 0 = some ff

@[simp]

theorem encodable.decode_one :

encodable.decode bool 1 = some tt

theorem encodable.decode_ge_two (n : ℕ) (h : 2 ≤ n) :

encodable.decode bool n = none

def encodable.encode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :

sigma γ → ℕ

Equations

encodable.encode_sigma ⟨a, b⟩ = (encodable.encode a).mkpair (encodable.encode b)

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

option (sigma γ)

Equations

encodable.decode_sigma n = encodable.decode_sigma._match_1 n.unpair
encodable.decode_sigma._match_1 (n₁, n₂) = (encodable.decode α n₁).bind (λ (a : α), option.map (sigma.mk a) (encodable.decode (γ a) n₂))

@[protected, instance]

def encodable.sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :

encodable (sigma γ)

Equations

encodable.sigma = {encode := encodable.encode_sigma (λ (a : α), _inst_2 a), decode := encodable.decode_sigma (λ (a : α), _inst_2 a), encodek := _}

@[simp]

theorem encodable.decode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ℕ) :

encodable.decode (sigma γ) n = (encodable.decode α n.unpair.fst).bind (λ (a : α), option.map (sigma.mk 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) :

encodable.encode ⟨a, b⟩ = (encodable.encode a).mkpair (encodable.encode b)

@[protected, instance]

def encodable.prod {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :

encodable (α × β)

Equations

encodable.prod = encodable.of_equiv (Σ (_x : α), β) (equiv.sigma_equiv_prod α β).symm

@[simp]

theorem encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ℕ) :

encodable.decode (α × β) n = (encodable.decode α n.unpair.fst).bind (λ (a : α), option.map (prod.mk a) (encodable.decode β n.unpair.snd))

@[simp]

theorem encodable.encode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) (b : β) :

encodable.encode (a, b) = (encodable.encode a).mkpair (encodable.encode b)

def encodable.encode_subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] :

{a // P a} → ℕ

Equations

encodable.encode_subtype ⟨v, h⟩ = encodable.encode v

def encodable.decode_subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] (v : ℕ) :

option {a // P a}

Equations

encodable.decode_subtype v = (encodable.decode α v).bind (λ (a : α), dite (P a) (λ (h : P a), some ⟨a, h⟩) (λ (h : ¬P a), none))

@[protected, instance]

def encodable.subtype {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] :

encodable {a // P a}

Equations

encodable.subtype = {encode := encodable.encode_subtype encA, decode := encodable.decode_subtype (λ (a : α), decP a), encodek := _}

theorem encodable.subtype.encode_eq {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] (a : subtype P) :

encodable.encode a = encodable.encode a.val

@[protected, instance]

def encodable.fin (n : ℕ) :

encodable (fin n)

Equations

encodable.fin n = encodable.of_equiv {m // m < n} (equiv.fin_equiv_subtype n)

@[protected, instance]

def encodable.int :

Equations

encodable.int = encodable.of_equiv ℕ equiv.int_equiv_nat

@[protected, instance]

def encodable.ulift {α : Type u_1} [encodable α] :

encodable (ulift α)

Equations

encodable.ulift = encodable.of_equiv α equiv.ulift

@[protected, instance]

def encodable.plift {α : Type u_1} [encodable α] :

encodable (plift α)

Equations

encodable.plift = encodable.of_equiv α equiv.plift

def encodable.of_inj {α : Type u_1} {β : Type u_2} [encodable β] (f : α → β) (hf : function.injective f) :

Equations

encodable.of_inj f hf = encodable.of_left_injection f (function.partial_inv f) _

@[protected, instance]

def ulower.decidable_eq (α : Type u_1) [encodable α] :

decidable_eq (ulower α)

def ulower (α : Type u_1) [encodable α] :

Type

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

Equations

ulower α = ↥(set.range encodable.encode)

@[protected, instance]

def ulower.encodable (α : Type u_1) [encodable α] :

encodable (ulower α)

def ulower.equiv (α : Type u_1) [encodable α] :

α ≃ ulower α

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

Equations

ulower.equiv α = encodable.equiv_range_encode α

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

Lowers an a : α into ulower α.

Equations

ulower.down a = ⇑(ulower.equiv α) a

@[protected, instance]

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

inhabited (ulower α)

Equations

ulower.inhabited = {default := ulower.down (default α)}

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

α

Lifts an a : ulower α into α.

Equations

a.up = ⇑((ulower.equiv α).symm) a

@[simp]

theorem ulower.down_up {α : Type u_1} [encodable α] {a : ulower α} :

ulower.down a.up = a

@[simp]

theorem ulower.up_down {α : Type u_1} [encodable α] {a : α} :

(ulower.down a).up = 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 : α} :

ulower.down a = ulower.down b ↔ a = b

@[protected, ext]

theorem ulower.ext {α : Type u_1} [encodable α] {a b : ulower α} :

a.up = b.up → a = b

def encodable.choose_x {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :

{a // p a}

Equations

encodable.choose_x h = have this : ∃ (n : ℕ), good p (encodable.decode α n), from _, encodable.choose_x._match_4 (encodable.decode α (nat.find this)) _
encodable.choose_x._match_4 (some a) h = ⟨a, h⟩
_ = _

def encodable.choose {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :

α

Equations

encodable.choose h = (encodable.choose_x h).val

theorem encodable.choose_spec {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :

p (encodable.choose h)

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

encodable.encode' α = {to_fun := encodable.encode _inst_1, inj' := _}

@[protected, instance]

def encodable.order.preimage.is_trans {α : Type u_1} [encodable α] :

is_trans α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

@[protected, instance]

def encodable.order.preimage.is_antisymm {α : Type u_1} [encodable α] :

is_antisymm α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

@[protected, instance]

def encodable.order.preimage.is_total {α : Type u_1} [encodable α] :

is_total α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

@[protected]

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

directed.sequence f hf (n + 1) = let p : α := directed.sequence f hf n in directed.sequence._match_1 f hf p (encodable.decode α n)
directed.sequence f hf 0 = default α
directed.sequence._match_1 f hf p (some a) = classical.some _
directed.sequence._match_1 f hf p none = classical.some _

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) :

monotone (f ∘ directed.sequence f hf)

theorem directed.le_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : directed has_le.le f) (a : α) :

f a ≤ f (directed.sequence f hf (encodable.encode a + 1))

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

q.rep = encodable.choose _

theorem quotient.rep_spec {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [encodable α] (q : quotient s) :

⟦q.rep ⟧ = q

def encodable_quotient {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [encodable α] :

encodable (quotient s)

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

Equations

encodable_quotient = {encode := λ (q : quotient s), encodable.encode q.rep, decode := λ (n : ℕ), quotient.mk <$> encodable.decode α n, encodek := _}