# Documentation

Mathlib.Data.Set.Countable

# Countable sets #

def Set.Countable {α : Type u} (s : Set α) :

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
Instances For
@[simp]
theorem Set.countable_coe_iff {α : Type u} {s : Set α} :
theorem Set.to_countable {α : Type u} (s : Set α) [] :

Prove Set.Countable from a Countable instance on the subtype.

theorem Countable.to_set {α : Type u} {s : Set α} :

Restate Set.Countable as a Countable instance.

theorem Set.Countable.to_subtype {α : Type u} {s : Set α} :

Restate Set.Countable as a Countable instance.

theorem Set.countable_iff_exists_injective {α : Type u} {s : Set α} :
∃ (f : s),
theorem Set.countable_iff_exists_injOn {α : Type u} {s : Set α} :
∃ (f : α),

A set s : Set α is countable if and only if there exists a function α → ℕ injective on s.

def Set.Countable.toEncodable {α : Type u} {s : Set α} :

Convert Set.Countable s to Encodable s (noncomputable).

Equations
• Set.Countable.toEncodable = Classical.choice
Instances For
def Set.enumerateCountable {α : Type u} {s : Set α} (h : ) (default : α) :
α

Noncomputably enumerate elements in a set. The default value is used to extend the domain to all of ℕ.

Equations
Instances For
theorem Set.subset_range_enumerate {α : Type u} {s : Set α} (h : ) (default : α) :
theorem Set.Countable.mono {α : Type u} {s₁ : Set α} {s₂ : Set α} (h : s₁ s₂) :
theorem Set.countable_range {β : Type v} {ι : Sort x} [] (f : ιβ) :
theorem Set.countable_iff_exists_subset_range {α : Type u} [] {s : Set α} :
∃ (f : α), s
theorem Set.countable_iff_exists_surjective {α : Type u} {s : Set α} (hs : ) :
∃ (f : s),

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

theorem Set.Countable.exists_surjective {α : Type u} {s : Set α} (hs : ) :
∃ (f : s),

Alias of the forward direction of Set.countable_iff_exists_surjective.

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

theorem Set.countable_univ {α : Type u} [] :
Set.Countable Set.univ
theorem Set.Countable.exists_eq_range {α : Type u} {s : Set α} (hc : ) (hs : ) :
∃ (f : α), s =

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.image {α : Type u} {β : Type v} {s : Set α} (hs : ) (f : αβ) :
theorem Set.MapsTo.countable_of_injOn {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : αβ} (hf : Set.MapsTo f s t) (hf' : ) (ht : ) :
theorem Set.Countable.preimage_of_injOn {α : Type u} {β : Type v} {s : Set β} (hs : ) {f : αβ} (hf : Set.InjOn f (f ⁻¹' s)) :
theorem Set.Countable.preimage {α : Type u} {β : Type v} {s : Set β} (hs : ) {f : αβ} (hf : ) :
theorem Set.exists_seq_iSup_eq_top_iff_countable {α : Type u} [] {p : αProp} (h : ∃ (x : α), p x) :
(∃ (s : α), (∀ (n : ), p (s n)) ⨆ (n : ), s n = ) ∃ (S : Set α), (sS, p s) sSup 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 α)), (sS, p s) ⋃₀ S = Set.univ
theorem Set.countable_of_injective_of_countable_image {α : Type u} {β : Type v} {s : Set α} {f : αβ} (hf : ) (hs : Set.Countable (f '' s)) :
theorem Set.countable_iUnion {α : Type u} {ι : Sort x} {t : ιSet α} [] (ht : ∀ (i : ι), Set.Countable (t i)) :
Set.Countable (⋃ (i : ι), t i)
@[simp]
theorem Set.countable_iUnion_iff {α : Type u} {ι : Sort x} [] {t : ιSet α} :
Set.Countable (⋃ (i : ι), t i) ∀ (i : ι), Set.Countable (t i)
theorem Set.Countable.biUnion_iff {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a sSet β} (hs : ) :
Set.Countable (⋃ (a : α), ⋃ (h : a s), t a h) ∀ (a : α) (ha : a s), Set.Countable (t a ha)
theorem Set.Countable.sUnion_iff {α : Type u} {s : Set (Set α)} (hs : ) :
Set.Countable (⋃₀ s) as,
theorem Set.Countable.biUnion {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a sSet β} (hs : ) :
(∀ (a : α) (ha : a s), Set.Countable (t a ha))Set.Countable (⋃ (a : α), ⋃ (h : a s), t a h)

Alias of the reverse direction of Set.Countable.biUnion_iff.

theorem Set.Countable.sUnion {α : Type u} {s : Set (Set α)} (hs : ) :
(as, )Set.Countable (⋃₀ s)

Alias of the reverse direction of Set.Countable.sUnion_iff.

@[simp]
theorem Set.countable_union {α : Type u} {s : Set α} {t : Set α} :
theorem Set.Countable.union {α : Type u} {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem Set.Countable.of_diff {α : Type u} {s : Set α} {t : Set α} (h : Set.Countable (s \ t)) (ht : ) :
@[simp]
theorem Set.countable_insert {α : Type u} {s : Set α} {a : α} :
theorem Set.Countable.insert {α : Type u} {s : Set α} (a : α) (h : ) :
theorem Set.Finite.countable {α : Type u} {s : Set α} :
theorem Set.Countable.of_subsingleton {α : Type u} [] (s : Set α) :
theorem Set.Subsingleton.countable {α : Type u} {s : Set α} (hs : ) :
theorem Set.countable_isTop (α : Type u_1) [] :
Set.Countable {x : α | }
theorem Set.countable_isBot (α : Type u_1) [] :
Set.Countable {x : α | }
theorem Set.countable_setOf_finite_subset {α : Type u} {s : Set α} (hs : ) :
Set.Countable {t : Set α | t s}

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

theorem Set.countable_univ_pi {α : Type u} {π : αType u_1} [] {s : (a : α) → Set (π a)} (hs : ∀ (a : α), Set.Countable (s a)) :
Set.Countable (Set.pi Set.univ s)
theorem Set.countable_pi {α : Type u} {π : αType u_1} [] {s : (a : α) → Set (π a)} (hs : ∀ (a : α), Set.Countable (s a)) :
Set.Countable {f : (a : α) → π a | ∀ (a : α), f a s a}
theorem Set.Countable.prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem Set.Countable.image2 {α : Type u} {β : Type v} {γ : Type w} {s : Set α} {t : Set β} (hs : ) (ht : ) (f : αβγ) :
theorem Set.countable_setOf_nonempty_of_disjoint {α : Type u} {β : Type v} {f : βSet α} (hf : Pairwise (Disjoint on f)) {s : Set α} (h'f : ∀ (t : β), f t s) (hs : ) :
Set.Countable {t : β | Set.Nonempty (f t)}

If a family of disjoint sets is included in a countable set, then only countably many of them are nonempty.

theorem Finset.countable_toSet {α : Type u} (s : ) :