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