Countable types #
In this file we define a typeclass saying that a given Sort _
is countable. See also Encodable
for a version that singles out a specific encoding of elements of α
by natural numbers.
This file also provides a few instances of this typeclass. More instances can be found in other files.
Definition and basic properties #
theorem
Function.Injective.countable
{α : Sort u}
{β : Sort v}
[inst : Countable β]
{f : α → β}
(hf : Function.Injective f)
:
theorem
Function.Surjective.countable
{α : Sort u}
{β : Sort v}
[inst : Countable α]
{f : α → β}
(hf : Function.Surjective f)
:
theorem
exists_surjective_nat
(α : Sort u)
[inst : Nonempty α]
[inst : Countable α]
:
∃ f, Function.Surjective f
theorem
countable_iff_exists_surjective
{α : Sort u}
[inst : Nonempty α]
:
Countable α ↔ ∃ f, Function.Surjective f
Operations on Sort _
s #
Equations
Equations
- instCountablePUnit = (_ : Countable PUnit)