Denumerable types #
This file defines denumerable (countably infinite) types as a typeclass extending encodable. This
is used to provide explicit encode/decode functions from and to ℕ, with the information that those
functions are inverses of each other.
Implementation notes #
This property already has a name, namely α ≃ ℕ, but here we are interested in using it as a
typeclass.
@[class]
- to_encodable : encodable α
- decode_inv : ∀ (n : ℕ), ∃ (a : α) (H : a ∈ encodable.decode α n), encodable.encode a = n
A denumerable type is (constructively) bijective with ℕ. Typeclass equivalent of α ≃ ℕ.
theorem
denumerable.decode_is_some
(α : Type u_1)
[denumerable α]
(n : ℕ) :
↥((encodable.decode α n).is_some)
Returns the n-th element of α indexed by the decoding.
Equations
- denumerable.of_nat α n = option.get _
@[simp]
theorem
denumerable.decode_eq_of_nat
(α : Type u_1)
[denumerable α]
(n : ℕ) :
encodable.decode α n = some (denumerable.of_nat α n)
@[simp]
theorem
denumerable.of_nat_of_decode
{α : Type u_1}
[denumerable α]
{n : ℕ}
{b : α}
(h : encodable.decode α n = some b) :
denumerable.of_nat α n = b
@[simp]
theorem
denumerable.encode_of_nat
{α : Type u_1}
[denumerable α]
(n : ℕ) :
encodable.encode (denumerable.of_nat α n) = n
@[simp]
theorem
denumerable.of_nat_encode
{α : Type u_1}
[denumerable α]
(a : α) :
denumerable.of_nat α (encodable.encode a) = a
A denumerable type is equivalent to ℕ.
Equations
- denumerable.eqv α = {to_fun := encodable.encode denumerable.to_encodable, inv_fun := denumerable.of_nat α _inst_3, left_inv := _, right_inv := _}
A type equivalent to ℕ is denumerable.
Equations
- denumerable.mk' e = {to_encodable := {encode := ⇑e, decode := some ∘ ⇑(e.symm), encodek := _}, decode_inv := _}
Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable way.
Equations
- denumerable.of_equiv α e = {to_encodable := {encode := encodable.encode (encodable.of_equiv α e), decode := encodable.decode β (encodable.of_equiv α e), encodek := _}, decode_inv := _}
@[simp]
theorem
denumerable.of_equiv_of_nat
(α : Type u_1)
{β : Type u_2}
[denumerable α]
(e : β ≃ α)
(n : ℕ) :
denumerable.of_nat β n = ⇑(e.symm) (denumerable.of_nat α n)
All denumerable types are equivalent.
Equations
- denumerable.equiv₂ α β = (denumerable.eqv α).trans (denumerable.eqv β).symm
@[protected, instance]
Equations
- denumerable.nat = {to_encodable := encodable.nat, decode_inv := denumerable.nat._proof_1}
@[protected, instance]
def
denumerable.sum
{α : Type u_1}
{β : Type u_2}
[denumerable α]
[denumerable β] :
denumerable (α ⊕ β)
If α and β are denumerable, then so is their sum.
Equations
@[protected, instance]
def
denumerable.sigma
{α : Type u_1}
[denumerable α]
{γ : α → Type u_3}
[Π (a : α), denumerable (γ a)] :
denumerable (sigma γ)
A denumerable collection of denumerable types is denumerable.
Equations
- denumerable.sigma = {to_encodable := encodable.sigma (λ (a : α), denumerable.to_encodable), decode_inv := _}
@[simp]
theorem
denumerable.sigma_of_nat_val
{α : Type u_1}
[denumerable α]
{γ : α → Type u_3}
[Π (a : α), denumerable (γ a)]
(n : ℕ) :
denumerable.of_nat (sigma γ) n = ⟨denumerable.of_nat α (nat.unpair n).fst, denumerable.of_nat (γ (denumerable.of_nat α (nat.unpair n).fst)) (nat.unpair n).snd⟩
@[protected, instance]
def
denumerable.prod
{α : Type u_1}
{β : Type u_2}
[denumerable α]
[denumerable β] :
denumerable (α × β)
If α and β are denumerable, then so is their product.
Equations
- denumerable.prod = denumerable.of_equiv (Σ (_x : α), β) (equiv.sigma_equiv_prod α β).symm
@[simp]
theorem
denumerable.prod_of_nat_val
{α : Type u_1}
{β : Type u_2}
[denumerable α]
[denumerable β]
(n : ℕ) :
denumerable.of_nat (α × β) n = (denumerable.of_nat α (nat.unpair n).fst, denumerable.of_nat β (nat.unpair n).snd)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
The lift of a denumerable type is denumerable.
Equations
@[protected, instance]
The lift of a denumerable type is denumerable.
Equations
If α is denumerable, then α × α and α are equivalent.
Equations
- denumerable.pair = denumerable.equiv₂ (α × α) α
Subsets of ℕ #
theorem
nat.subtype.succ_le_of_lt
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)]
{x y : ↥s}
(h : y < x) :
nat.subtype.succ y ≤ x
theorem
nat.subtype.le_succ_of_forall_lt_le
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)]
{x y : ↥s}
(h : ∀ (z : ↥s), z < x → z ≤ y) :
x ≤ nat.subtype.succ y
theorem
nat.subtype.lt_succ_self
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)]
(x : ↥s) :
x < nat.subtype.succ x
theorem
nat.subtype.lt_succ_iff_le
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)]
{x y : ↥s} :
x < nat.subtype.succ y ↔ x ≤ y
Returns the n-th element of a set, according to the usual ordering of ℕ.
Equations
- nat.subtype.of_nat s (n + 1) = nat.subtype.succ (nat.subtype.of_nat s n)
- nat.subtype.of_nat s 0 = ⊥
theorem
nat.subtype.of_nat_surjective_aux
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)]
{x : ℕ}
(hx : x ∈ s) :
∃ (n : ℕ), nat.subtype.of_nat s n = ⟨x, hx⟩
theorem
nat.subtype.of_nat_surjective
{s : set ℕ}
[infinite ↥s]
[decidable_pred (λ (_x : ℕ), _x ∈ s)] :
Any infinite set of naturals is denumerable.
Equations
- nat.subtype.denumerable s = denumerable.of_equiv ℕ {to_fun := to_fun_aux (λ (a : ℕ), _inst_3 a), inv_fun := nat.subtype.of_nat s _inst_4, left_inv := _, right_inv := _}
An infinite encodable type is denumerable.
Equations
- denumerable.of_encodable_of_infinite α = let _inst : decidable_pred (λ (_x : ℕ), _x ∈ set.range encodable.encode) := encodable.decidable_range_encode α, _inst_3 : infinite ↥(set.range encodable.encode) := _, _inst_4 : denumerable ↥(set.range encodable.encode) := nat.subtype.denumerable (set.range encodable.encode) in denumerable.of_equiv ↥(set.range encodable.encode) (encodable.equiv_range_encode α)