mathlib documentation

data.set.countable

Countable sets #

def set.countable {α : Type u} (s : 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

s.countable = nonempty (encodable ↥s)

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 α} (hs : 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.

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

s.countable → encodable ↥s

Convert countable s to encodable s (noncomputable).

Equations

set.countable.to_encodable = classical.choice

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 α} (hc : s.countable) (hs : s.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 α} (h : s₁ ⊆ s₂) :

s₂.countable → s₁.countable

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

(f '' s).countable

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

(set.range f).countable

theorem set.maps_to.countable_of_inj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (hf : set.maps_to f s t) (hf' : set.inj_on f s) (ht : t.countable) :

theorem set.countable.preimage_of_inj_on {α : Type u} {β : Type v} {s : set β} (hs : s.countable) {f : α → β} (hf : set.inj_on f (f ⁻¹' s)) :

(f ⁻¹' s).countable

@[protected]

theorem set.countable.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.countable) {f : α → β} (hf : function.injective f) :

(f ⁻¹' s).countable

theorem set.exists_seq_supr_eq_top_iff_countable {α : Type u} [complete_lattice α] {p : α → Prop} (h : ∃ (x : α), p x) :

(∃ (s : ℕ → α), (∀ (n : ℕ), p (s n)) ∧ (⨆ (n : ℕ), s n) = ⊤) ↔ ∃ (S : set α), S.countable ∧ (∀ (s : α), s ∈ S → p s) ∧ Sup S = ⊤

theorem set.exists_seq_cover_iff_countable {α : Type u} {p : set α → Prop} (h : ∃ (s : set α), p s) :

(∃ (s : ℕ → set α), (∀ (n : ℕ), p (s n)) ∧ (⋃ (n : ℕ), s n) = set.univ) ↔ ∃ (S : set (set α)), S.countable ∧ (∀ (s : set α), s ∈ S → p s) ∧ ⋃₀S = set.univ

theorem set.countable_of_injective_of_countable_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (hf : set.inj_on f s) (hs : (f '' s).countable) :

theorem set.countable_Union {α : Type u} {β : Type v} {t : α → set β} [encodable α] (ht : ∀ (a : α), (t a).countable) :

(⋃ (a : α), t a).countable

theorem set.countable.bUnion {α : Type u} {β : Type v} {s : set α} {t : Π (x : α), x ∈ s → set β} (hs : s.countable) (ht : ∀ (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 α)} (hs : s.countable) (h : ∀ (a : set α), a ∈ s → a.countable) :

(⋃₀s).countable

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

(⋃ (h : p), t h).countable

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

(s₁ ∪ s₂).countable

@[simp]

theorem set.countable_union {α : Type u} {s t : set α} :

(s ∪ t).countable ↔ s.countable ∧ t.countable

@[simp]

theorem set.countable_insert {α : Type u} {s : set α} {a : α} :

(insert a s).countable ↔ s.countable

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

(insert a s).countable

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

s.finite → s.countable

theorem set.subsingleton.countable {α : Type u} {s : set α} (hs : s.subsingleton) :

theorem set.countable_is_top (α : Type u_1) [partial_order α] :

{x : α | is_top x}.countable

theorem set.countable_is_bot (α : Type u_1) [partial_order α] :

{x : α | is_bot x}.countable

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)} (hs : ∀ (a : α), (s a).countable) :

{f : Π (a : α), π a | ∀ (a : α), f a ∈ s a}.countable

@[protected]

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

(s ×ˢ t).countable

theorem set.countable.image2 {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} (hs : s.countable) (ht : t.countable) (f : α → β → γ) :

(set.image2 f s t).countable

noncomputable def set.enumerate_countable {α : Type u} {s : set α} (h : s.countable) (default : α) :

ℕ → α

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 (some y) = ↑y
set.enumerate_countable._match_1 default none = default

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

s ⊆ set.range (set.enumerate_countable h default)

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