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.
- encode : α → ℕ
- encodek : ∀ (a : α), Encodable.decode (Encodable.encode a) = some a
- decode_inv : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decode n ∧ Encodable.encode a = n
decode
andencode
are inverses.
A denumerable type is (constructively) bijective with ℕ
. Typeclass equivalent of α ≃ ℕ
.
Instances
Returns the n
-th element of α
indexed by the decoding.
Instances For
A denumerable type is equivalent to ℕ
.
Instances For
A type equivalent to ℕ
is denumerable.
Instances For
Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable way.
Instances For
All denumerable types are equivalent.
Instances For
If α
is denumerable, then so is Option α
.
If α
and β
are denumerable, then so is their sum.
A denumerable collection of denumerable types is denumerable.
If α
and β
are denumerable, then so is their product.
The lift of a denumerable type is denumerable.
The lift of a denumerable type is denumerable.
If α
is denumerable, then α × α
and α
are equivalent.
Instances For
Subsets of ℕ
#
Returns the next natural in a set, according to the usual ordering of ℕ
.
Instances For
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)
Instances For
Any infinite set of naturals is denumerable.
Instances For
An infinite encodable type is denumerable.
Instances For
See also nonempty_encodable
, nonempty_fintype
.