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.
- 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 α ≃ ℕ
.
Instances of this typeclass
Instances of other typeclasses for denumerable
- denumerable.has_sizeof_inst
Returns the n
-th element of α
indexed by the decoding.
Equations
- denumerable.of_nat α n = option.get _
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 := option.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 := _}
All denumerable types are equivalent.
Equations
- denumerable.equiv₂ α β = (denumerable.eqv α).trans (denumerable.eqv β).symm
Equations
- denumerable.nat = {to_encodable := nat.encodable, decode_inv := denumerable.nat._proof_1}
If α
and β
are denumerable, then so is their sum.
Equations
A denumerable collection of denumerable types is denumerable.
Equations
- denumerable.sigma = {to_encodable := sigma.encodable (λ (a : α), denumerable.to_encodable), decode_inv := _}
If α
and β
are denumerable, then so is their product.
Equations
- denumerable.prod = denumerable.of_equiv (Σ (_x : α), β) (equiv.sigma_equiv_prod α β).symm
Equations
Equations
The lift of a denumerable type is denumerable.
Equations
The lift of a denumerable type is denumerable.
Equations
If α
is denumerable, then α × α
and α
are equivalent.
Equations
- denumerable.pair = denumerable.equiv₂ (α × α) α
Subsets of ℕ
#
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 = ⊥
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 α)