Countable sets #
A set is countable if there exists an encoding of the set into the natural numbers.
An encoding is an injection with a partial inverse, which can be viewed as a
constructive analogue of countability. (For the most part, theorems about
Countable will be classical and
Encodable will be constructive.)
Noncomputably enumerate elements in a set. The
default value is used to extend the domain to
Alias of the forward direction of
A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.
If a family of disjoint sets is included in a countable set, then only countably many of them are nonempty.