# Countable sets #

In this file we define `Set.Countable s` as `Countable s` and prove basic properties of this definition.

Note that this definition does not provide a computable encoding. For a noncomputable conversion to `Encodable s`, use `Set.Countable.nonempty_encodable`.

## Keywords #

sets, countable set

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

A set `s` is countable if the corresponding subtype is countable, i.e., there exists an injective map `f : s → ℕ`.

Note that this is an abbreviation, so `hs : Set.Countable s` in the proof context is the same as an instance `Countable s`. For a constructive version, see `Encodable`.

Equations

- s.Countable = Countable ↑s

Instances For

source
@[simp]
theorem Set.countable_coe_iff {α : Type u} {s : Set α} :
Countable ↑s ↔ s.Countable
source
theorem Set.to_countable {α : Type u} (s : Set α) [Countable ↑s] :
s.Countable

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

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

Restate `Set.Countable` as a `Countable` instance.

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

Restate `Set.Countable` as a `Countable` instance.

source
theorem Set.countable_iff_exists_injective {α : Type u} {s : Set α} :
s.Countable ↔ ∃ (f : ↑s → ℕ), Function.Injective f
source
theorem Set.countable_iff_exists_injOn {α : Type u} {s : Set α} :
s.Countable ↔ ∃ (f : α → ℕ), InjOn f s

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

source
theorem Set.countable_iff_nonempty_encodable {α : Type u} {s : Set α} :
s.Countable ↔ Nonempty (Encodable ↑s)
source
theorem Set.Countable.nonempty_encodable {α : Type u} {s : Set α} :
s.Countable → Nonempty (Encodable ↑s)

Alias of the forward direction of `Set.countable_iff_nonempty_encodable`.

source
def Set.Countable.toEncodable {α : Type u} {s : Set α} (hs : s.Countable) :
Encodable ↑s

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

Equations

- hs.toEncodable = Classical.choice ⋯

Instances For

source
def Set.enumerateCountable {α : 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

- Set.enumerateCountable h default n = match Encodable.decode n with | some y => ↑y | none => default

Instances For

source
theorem Set.subset_range_enumerate {α : Type u} {s : Set α} (h : s.Countable) (default : α) :
s ⊆ range (enumerateCountable h default)
source
theorem Set.range_enumerateCountable_subset {α : Type u} {s : Set α} (h : s.Countable) (default : α) :
range (enumerateCountable h default) ⊆ insert default s
source
theorem Set.range_enumerateCountable_of_mem {α : Type u} {s : Set α} (h : s.Countable) {default : α} (h_mem : default ∈ s) :
range (enumerateCountable h default) = s
source
theorem Set.enumerateCountable_mem {α : Type u} {s : Set α} (h : s.Countable) {default : α} (h_mem : default ∈ s) (n : ℕ) :
enumerateCountable h default n ∈ s
source
theorem Set.Countable.mono {α : Type u} {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (hs : s₂.Countable) :
s₁.Countable
source
theorem Set.countable_range {β : Type v} {ι : Sort x} [Countable ι] (f : ι → β) :
(range f).Countable
source
theorem Set.countable_iff_exists_subset_range {α : Type u} [Nonempty α] {s : Set α} :
s.Countable ↔ ∃ (f : ℕ → α), s ⊆ range f
source
theorem Set.countable_iff_exists_surjective {α : 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.

source
theorem Set.Countable.exists_surjective {α : Type u} {s : Set α} (hs : s.Nonempty) :
s.Countable → ∃ (f : ℕ → ↑s), Function.Surjective f

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.

source
theorem Set.countable_univ_iff {α : Type u} :
univ.Countable ↔ Countable α
source
theorem Set.countable_univ {α : Type u} [Countable α] :
univ.Countable
source
theorem Set.not_countable_univ_iff {α : Type u} :
¬univ.Countable ↔ Uncountable α
source
theorem Set.not_countable_univ {α : Type u} [Uncountable α] :
¬univ.Countable
source
theorem Set.Countable.exists_eq_range {α : Type u} {s : Set α} (hc : s.Countable) (hs : s.Nonempty) :
∃ (f : ℕ → α), s = range f

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

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

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

source
theorem Set.Countable.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Countable) :
(∀ a ∈ s, a.Countable) → (⋃₀ s).Countable

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

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

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

source
theorem Set.Countable.setOf_finite {α : Type u} [Countable α] :
{s : Set α | s.Finite}.Countable

The set of finite sets in a countable type is countable.

source
theorem Set.countable_univ_pi {α : Type u} {π : α → Type u_1} [Finite α] {s : (a : α) → Set (π a)} (hs : ∀ (a : α), (s a).Countable) :
(univ.pi s).Countable
source
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
source
theorem Set.Countable.prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : s.Countable) (ht : t.Countable) :
(s ×ˢ t).Countable
source
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
source
theorem Set.countable_setOf_nonempty_of_disjoint {α : Type u} {β : Type v} {f : β → Set α} (hf : Pairwise (Function.onFun Disjoint f)) {s : Set α} (h'f : ∀ (t : β), f t ⊆ s) (hs : s.Countable) :
{t : β | (f t).Nonempty}.Countable

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

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