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.)
theorem
set.countable_iff_exists_injective
{α : Type u}
{s : set α} :
s.countable ↔ ∃ (f : ↥s → ℕ), function.injective f
theorem
set.countable_iff_exists_inj_on
{α : Type u}
{s : set α} :
s.countable ↔ ∃ (f : α → ℕ), set.inj_on f s
A set s : set α is countable if and only if there exists a function α → ℕ injective
on s.
A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.
Convert countable s to encodable s (noncomputable).
Equations
theorem
set.countable_of_injective_of_countable_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s → (f '' s).countable → s.countable
theorem
set.countable.insert
{α : Type u}
{s : set α}
(a : α) :
s.countable → (has_insert.insert a s).countable
Enumerate elements in a countable set.
Equations
- set.enumerate_countable h default = λ (n : ℕ), set.enumerate_countable._match_1 default (encodable.decode ↥s n)
- set.enumerate_countable._match_1 default (option.some y) = ↑y
- set.enumerate_countable._match_1 default option.none = default
theorem
set.subset_range_enumerate
{α : Type u}
{s : set α}
(h : s.countable)
(default : α) :
s ⊆ set.range (set.enumerate_countable h default)