mathlib documentation

data.set.countable

Countable sets

def set.countable {α : Type u} :
set α → Prop

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.)

Equations
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.

theorem set.countable_iff_exists_surjective {α : Type u} [ne : nonempty α] {s : set α} :
s.countable ∃ (f : → α), s set.range f

theorem set.countable_iff_exists_surjective_to_subtype {α : Type u} {s : set α} :
s.nonempty(s.countable ∃ (f : s), function.surjective f)

A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.

def set.countable.to_encodable {α : Type u} {s : set α} :

Convert countable s to encodable s (noncomputable).

Equations
theorem set.countable_encodable' {α : Type u} (s : set α) [H : encodable s] :

theorem set.countable_encodable {α : Type u} [encodable α] (s : set α) :

theorem set.countable.exists_surjective {α : Type u} {s : set α} :
s.countables.nonempty(∃ (f : → α), s = set.range f)

If s : set α is a nonempty countable set, then there exists a map f : ℕ → α such that s = range f.

@[simp]
theorem set.countable_empty {α : Type u} :

@[simp]
theorem set.countable_singleton {α : Type u} (a : α) :

theorem set.countable.mono {α : Type u} {s₁ s₂ : set α} :
s₁ s₂s₂.countable → s₁.countable

theorem set.countable.image {α : Type u} {β : Type v} {s : set α} (hs : s.countable) (f : α → β) :

theorem set.countable_range {α : Type u} {β : Type v} [encodable α] (f : α → β) :

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_Union {α : Type u} {β : Type v} {t : α → set β} [encodable α] :
(∀ (a : α), (t a).countable)(⋃ (a : α), t a).countable

theorem set.countable.bUnion {α : Type u} {β : Type v} {s : set α} {t : Π (x : α), x sset β} :
s.countable(∀ (a : α) (H : a s), (t a H).countable)(⋃ (a : α) (H : a s), t a H).countable

theorem set.countable.sUnion {α : Type u} {s : set (set α)} :
s.countable(∀ (a : set α), a s → a.countable) → (⋃₀s).countable

theorem set.countable_Union_Prop {β : Type v} {p : Prop} {t : p → set β} :
(∀ (h : p), (t h).countable)(⋃ (h : p), t h).countable

theorem set.countable.union {α : Type u} {s₁ s₂ : set α} :
s₁.countables₂.countable(s₁ s₂).countable

theorem set.countable.insert {α : Type u} {s : set α} (a : α) :

theorem set.finite.countable {α : Type u} {s : set α} :

theorem set.countable_set_of_finite_subset {α : Type u} {s : set α} :
s.countable{t : set α | t.finite t s}.countable

The set of finite subsets of a countable set is countable.

theorem set.countable_pi {α : Type u} {π : α → Type u_1} [fintype α] {s : Π (a : α), set («π» a)} :
(∀ (a : α), (s a).countable){f : Π (a : α), «π» a | ∀ (a : α), f a s a}.countable

theorem set.countable_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
s.countablet.countable(s.prod t).countable

def set.enumerate_countable {α : Type u} {s : set α} :
s.countableα → → α

Enumerate elements in a countable set.

Equations
theorem set.subset_range_enumerate {α : Type u} {s : set α} (h : s.countable) (default : α) :

theorem finset.countable_to_set {α : Type u} (s : finset α) :