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.
decode
andencode
are inverses.decode_inv : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n
A denumerable type is (constructively) bijective with ℕ
. Typeclass equivalent of α ≃ ℕ≃ ℕ
.
Instances
Returns the n
-th element of α
indexed by the decoding.
Equations
- Denumerable.ofNat α n = Option.get (Encodable.decode n) (_ : Option.isSome (Encodable.decode n) = true)
A denumerable type is equivalent to ℕ
.
Equations
- One or more equations did not get rendered due to their size.
A type equivalent to ℕ
is denumerable.
Equations
- Denumerable.mk' e = Denumerable.mk (_ : ∀ (x : ℕ), ∃ a, a ∈ Encodable.decode x ∧ Encodable.encode a = x)
Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable way.
Equations
- Denumerable.ofEquiv α e = let src := Encodable.ofEquiv α e; Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)
All denumerable types are equivalent.
Equations
- Denumerable.equiv₂ α β = Equiv.trans (Denumerable.eqv α) (Equiv.symm (Denumerable.eqv β))
If α
is denumerable, then so is option α
.
Equations
- Denumerable.option = Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)
If α
and β
are denumerable, then so is their sum.
Equations
- Denumerable.sum = Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n)
A denumerable collection of denumerable types is denumerable.
Equations
- One or more equations did not get rendered due to their size.
If α
and β
are denumerable, then so is their product.
Equations
- Denumerable.prod = Denumerable.ofEquiv ((_ : α) × β) (Equiv.symm (Equiv.sigmaEquivProd α β))
Equations
The lift of a denumerable type is denumerable.
Equations
- Denumerable.ulift = Denumerable.ofEquiv α Equiv.ulift
The lift of a denumerable type is denumerable.
Equations
- Denumerable.plift = Denumerable.ofEquiv α Equiv.plift
If α
is denumerable, then α × α× α
and α
are equivalent.
Equations
- Denumerable.pair = Denumerable.equiv₂ (α × α) α
Subsets of ℕ
#
Returns the next natural in a set, according to the usual ordering of ℕ
.
Returns the n
-th element of a set, according to the usual ordering of ℕ
.
Equations
- Nat.Subtype.ofNat s 0 = ⊥
- Nat.Subtype.ofNat s (Nat.succ n) = Nat.Subtype.succ (Nat.Subtype.ofNat s n)
Any infinite set of naturals is denumerable.
Equations
- One or more equations did not get rendered due to their size.
An infinite encodable type is denumerable.
Equations
- Denumerable.ofEncodableOfInfinite α = Denumerable.ofEquiv (↑(Set.range Encodable.encode)) (Encodable.equivRangeEncode α)
See also nonempty_encodable
, nonempty_fintype
.