@[class]
- encode : α → ℕ
- decode : ℕ → option α
- encodek : ∀ (a : α), encodable.decode α (encodable.encode a) = option.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
- denumerable.to_encodable
- primcodable.to_encodable
- encodable.nat
- encodable.empty
- encodable.unit
- encodable.option
- encodable.sum
- encodable.bool
- encodable.sigma
- encodable.prod
- encodable.subtype
- encodable.fin
- encodable.int
- encodable.ulift
- encodable.plift
- ulower.encodable
- rat.encodable
- encodable.list
- encodable.multiset
- encodable.vector
- encodable.fin_arrow
- encodable.fin_pi
- encodable.array
- encodable.finset
- encodable.fintype_arrow_of_encodable
- encodable.encodable
Equations
def
encodable.of_left_injection
{α : Type u_1}
{β : Type u_2}
[encodable α]
(f : β → α)
(finv : α → option β) :
(∀ (b : β), finv (f b) = option.some b) → encodable β
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 : α → β) :
Equations
- encodable.of_left_inverse f finv linv = encodable.of_left_injection f (option.some ∘ finv) _
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)
@[instance]
Equations
- encodable.nat = {encode := id ℕ, decode := option.some ℕ, encodek := encodable.nat._proof_1}
@[instance]
@[instance]
Equations
- encodable.unit = {encode := λ (_x : punit), 0, decode := λ (n : ℕ), n.cases_on (option.some punit.star) (λ (_x : ℕ), option.none), encodek := encodable.unit._proof_1}
@[simp]
@[simp]
@[instance]
Equations
- encodable.option = {encode := λ (o : option α), o.cases_on 0 (λ (a : α), (encodable.encode a).succ), decode := λ (n : ℕ), n.cases_on (option.some option.none) (λ (m : ℕ), option.map option.some (encodable.decode α m)), encodek := _}
@[simp]
@[simp]
theorem
encodable.encode_some
{α : Type u_1}
[encodable α]
(a : α) :
encodable.encode (option.some a) = (encodable.encode a).succ
@[simp]
@[simp]
theorem
encodable.decode_option_succ
{α : Type u_1}
[encodable α]
(n : ℕ) :
encodable.decode (option α) n.succ = option.map option.some (encodable.decode α 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_inj
{α : Type u_1}
[encodable α]
{n : ℕ}
{a₁ a₂ : α} :
a₁ ∈ encodable.decode2 α n → a₂ ∈ encodable.decode2 α n → a₁ = a₂
Equations
- encodable.decidable_range_encode α = λ (x : ℕ), decidable_of_iff ↥((encodable.decode2 α x).is_some) _
Equations
- encodable.equiv_range_encode α = {to_fun := λ (a : α), ⟨encodable.encode a, _⟩, inv_fun := λ (n : ↥(set.range encodable.encode)), option.get _, left_inv := _, right_inv := _}
Equations
- encodable.encode_sum (sum.inr b) = bit1 (encodable.encode b)
- encodable.encode_sum (sum.inl a) = bit0 (encodable.encode a)
Equations
- encodable.decode_sum n = encodable.decode_sum._match_1 n.bodd_div2
- encodable.decode_sum._match_1 (bool.tt, m) = option.map sum.inr (encodable.decode β m)
- encodable.decode_sum._match_1 (bool.ff, m) = option.map sum.inl (encodable.decode α m)
@[instance]
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
@[instance]
def
encodable.encode_sigma
{α : Type u_1}
{γ : α → Type u_3}
[encodable α]
[Π (a : α), encodable (γ a)] :
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)] :
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₂))
@[instance]
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)
@[instance]
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)
Equations
def
encodable.decode_subtype
{α : Type u_1}
{P : α → Prop}
[encA : encodable α]
[decP : decidable_pred P] :
Equations
- encodable.decode_subtype v = (encodable.decode α v).bind (λ (a : α), dite (P a) (λ (h : P a), option.some ⟨a, h⟩) (λ (h : ¬P a), option.none))
@[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) :
@[instance]
Equations
- encodable.fin n = encodable.of_equiv {m // m < n} (equiv.fin_equiv_subtype n)
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
def
encodable.of_inj
{α : Type u_1}
{β : Type u_2}
[encodable β]
(f : α → β) :
function.injective f → encodable α
Equations
- encodable.of_inj f hf = encodable.of_left_injection f (function.partial_inv f) _
The equivalence between the encodable type α and ulower α : Type 0.
Equations
Lowers an a : α into ulower α.
Equations
- ulower.down a = ⇑(ulower.equiv α) a
@[instance]
Equations
@[simp]
@[simp]
@[simp]
theorem
ulower.down_eq_down
{α : Type u_1}
[encodable α]
{a b : α} :
ulower.down a = ulower.down b ↔ a = b
def
encodable.choose_x
{α : Type u_1}
{p : α → Prop}
[encodable α]
[decidable_pred p] :
(∃ (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 (option.some a) h = ⟨a, h⟩
- _ = _
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) :
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)] :
(∀ (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)
The encode function, viewed as an embedding.
Equations
- encodable.encode' α = {to_fun := encodable.encode _inst_1, inj' := _}
@[instance]
def
encodable.is_trans
{α : Type u_1}
[encodable α] :
is_trans α (⇑(encodable.encode' α) ⁻¹'o has_le.le)
Equations
@[instance]
def
encodable.is_antisymm
{α : Type u_1}
[encodable α] :
is_antisymm α (⇑(encodable.encode' α) ⁻¹'o has_le.le)
Equations
@[instance]
def
encodable.is_total
{α : Type u_1}
[encodable α] :
is_total α (⇑(encodable.encode' α) ⁻¹'o has_le.le)
Equations
def
directed.sequence
{α : Type u_1}
{β : Type u_2}
[encodable α]
[inhabited α]
{r : β → β → Prop}
(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 = inhabited.default α
- directed.sequence._match_1 f hf p (option.some a) = classical.some _
- directed.sequence._match_1 f hf p option.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 α] :
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) :
def
encodable_quotient
{α : Type u_1}
{s : setoid α}
[decidable_rel has_equiv.equiv]
[encodable α] :
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 := _}