# mathlib3documentation

data.set.countable

# Countable sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Prove set.countable from a countable instance on the subtype.

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

Restate set.countable as a countable instance.

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

Restate set.countable as a countable instance.

@[protected]
theorem set.countable_iff_exists_injective {α : Type u} {s : set α} :
theorem set.countable_iff_exists_inj_on {α : Type u} {s : set α} :
s.countable (f : α ), s

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

@[protected]
noncomputable def set.countable.to_encodable {α : Type u} {s : set α} :

Convert set.countable s to encodable s (noncomputable).

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

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

Equations
• default = λ (n : ), set.enumerate_countable._match_1 default 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 default)
theorem set.countable.mono {α : Type u} {s₁ s₂ : set α} (h : s₁ s₂) :
theorem set.countable_range {β : Type v} {ι : Sort x} [countable ι] (f : ι β) :
theorem set.countable_iff_exists_subset_range {α : Type u} [nonempty α] {s : set α} :
s.countable (f : α), s
@[protected]
theorem set.countable_iff_exists_surjective {α : Type u} {s : set α} (hs : s.nonempty) :

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 : s.nonempty) :

Alias of the forward direction of set.countable_iff_exists_surjective.

theorem set.countable_univ {α : Type u} [countable α] :
theorem set.countable.exists_eq_range {α : Type u} {s : set α} (hc : s.countable) (hs : s.nonempty) :
(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 : s.countable) (f : α β) :
theorem set.maps_to.countable_of_inj_on {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α β} (hf : s t) (hf' : s) (ht : t.countable) :
theorem set.countable.preimage_of_inj_on {α : Type u} {β : Type v} {s : set β} (hs : s.countable) {f : α β} (hf : (f ⁻¹' s)) :
@[protected]
theorem set.countable.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.countable) {f : α β} (hf : function.injective f) :
theorem set.exists_seq_supr_eq_top_iff_countable {α : Type u} {p : α Prop} (h : (x : α), p x) :
( (s : α), ( (n : ), p (s n)) ( (n : ), s n) = ) (S : set α), S.countable ( (s : α), s S p 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)
theorem set.countable_of_injective_of_countable_image {α : Type u} {β : Type v} {s : set α} {f : α β} (hf : s) (hs : (f '' s).countable) :
theorem set.countable_Union {α : Type u} {ι : Sort x} {t : ι set α} [countable ι] (ht : (i : ι), (t i).countable) :
( (i : ι), t i).countable
@[simp]
theorem set.countable_Union_iff {α : Type u} {ι : Sort x} [countable ι] {t : ι set α} :
( (i : ι), t i).countable (i : ι), (t i).countable
theorem set.countable.bUnion_iff {α : Type u} {β : Type v} {s : set α} {t : Π (a : α), a s set β} (hs : s.countable) :
( (a : α) (H : a s), t a H).countable (a : α) (H : a s), (t a H).countable
theorem set.countable.sUnion_iff {α : Type u} {s : set (set α)} (hs : s.countable) :
(⋃₀ s).countable (a : set α), a s a.countable
theorem set.countable.bUnion {α : Type u} {β : Type v} {s : set α} {t : Π (a : α), a s set β} (hs : s.countable) :
( (a : α) (H : a s), (t a H).countable) ( (a : α) (H : a s), t a H).countable

Alias of the reverse direction of set.countable.bUnion_iff.

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

Alias of the reverse direction of set.countable.sUnion_iff.

@[simp]
theorem set.countable_union {α : Type u} {s t : set α} :
theorem set.countable.union {α : Type u} {s t : set α} (hs : s.countable) (ht : t.countable) :
@[simp]
theorem set.countable_insert {α : Type u} {s : set α} {a : α} :
theorem set.countable.insert {α : Type u} {s : set α} (a : α) (h : s.countable) :
theorem set.finite.countable {α : Type u} {s : set α} :
theorem set.countable.of_subsingleton {α : Type u} [subsingleton α] (s : set α) :
theorem set.subsingleton.countable {α : Type u} {s : set α} (hs : s.subsingleton) :
theorem set.countable_is_top (α : Type u_1)  :
{x : α | is_top x}.countable
theorem set.countable_is_bot (α : Type u_1)  :
{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_univ_pi {α : Type u} {π : α Type u_1} [finite α] {s : Π (a : α), set (π a)} (hs : (a : α), (s a).countable) :
theorem set.countable_pi {α : Type u} {π : α Type u_1} [finite α] {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) :
theorem set.countable.image2 {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} (hs : s.countable) (ht : t.countable) (f : α β γ) :
s t).countable
theorem finset.countable_to_set {α : Type u} (s : finset α) :