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

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

• Set.Countable s = Countable ↑s

@[simp]

theorem Set.countable_coe_iff {α : Type u} {s : Set α} : Countable ↑s ↔ Set.Countable s

theorem Set.to_countable {α : Type u} (s : Set α) [Countable ↑s] : Set.Countable s

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

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

Restate Set.Countable as a Countable instance.

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

Restate Set.Countable as a Countable instance.

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

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

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

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

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

Alias of the forward direction of Set.countable_iff_nonempty_encodable.

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

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

Equations

• Set.Countable.toEncodable hs = Classical.choice ⋯

def Set.enumerateCountable {α : Type u} {s : Set α} (h : Set.Countable s) (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

theorem Set.subset_range_enumerate {α : Type u} {s : Set α} (h : Set.Countable s) (default : α) : s ⊆ Set.range (Set.enumerateCountable h default)

theorem Set.range_enumerateCountable_subset {α : Type u} {s : Set α} (h : Set.Countable s) (default : α) : Set.range (Set.enumerateCountable h default) ⊆ insert default s

theorem Set.range_enumerateCountable_of_mem {α : Type u} {s : Set α} (h : Set.Countable s) {default : α} (h_mem : default ∈ s) : Set.range (Set.enumerateCountable h default) = s

theorem Set.enumerateCountable_mem {α : Type u} {s : Set α} (h : Set.Countable s) {default : α} (h_mem : default ∈ s) (n : ℕ) : Set.enumerateCountable h default n ∈ s

theorem Set.Countable.mono {α : Type u} {s₁ : Set α} {s₂ : Set α} (h : s₁ ⊆ s₂) (hs : Set.Countable s₂) : Set.Countable s₁

theorem Set.countable_range {β : Type v} {ι : Sort x} [Countable ι] (f : ι → β) : Set.Countable (Set.range f)

theorem Set.countable_iff_exists_subset_range {α : Type u} [Nonempty α] {s : Set α} : Set.Countable s ↔ ∃ (f : ℕ → α), s ⊆ Set.range f

theorem Set.countable_iff_exists_surjective {α : Type u} {s : Set α} (hs : Set.Nonempty s) : Set.Countable s ↔ ∃ (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.

theorem Set.Countable.exists_surjective {α : Type u} {s : Set α} (hs : Set.Nonempty s) : Set.Countable s → ∃ (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.

theorem Set.countable_univ {α : Type u} [Countable α] : Set.Countable Set.univ

theorem Set.countable_univ_iff {α : Type u} : Set.Countable Set.univ ↔ Countable α

theorem Set.Countable.exists_eq_range {α : Type u} {s : Set α} (hc : Set.Countable s) (hs : Set.Nonempty s) : ∃ (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} : Set.Countable ∅

@[simp]

theorem Set.countable_singleton {α : Type u} (a : α) : Set.Countable {a}

theorem Set.Countable.image {α : Type u} {β : Type v} {s : Set α} (hs : Set.Countable s) (f : α → β) : Set.Countable (f '' s)

theorem Set.MapsTo.countable_of_injOn {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hf : Set.MapsTo f s t) (hf' : Set.InjOn f s) (ht : Set.Countable t) : Set.Countable s

theorem Set.Countable.preimage_of_injOn {α : Type u} {β : Type v} {s : Set β} (hs : Set.Countable s) {f : α → β} (hf : Set.InjOn f (f ⁻¹' s)) : Set.Countable (f ⁻¹' s)

theorem Set.Countable.preimage {α : Type u} {β : Type v} {s : Set β} (hs : Set.Countable s) {f : α → β} (hf : Function.Injective f) : Set.Countable (f ⁻¹' s)

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 α), Set.Countable S ∧ (∀ s ∈ S, 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 α)), Set.Countable S ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = Set.univ

theorem Set.countable_of_injective_of_countable_image {α : Type u} {β : Type v} {s : Set α} {f : α → β} (hf : Set.InjOn f s) (hs : Set.Countable (f '' s)) : Set.Countable s

theorem Set.countable_iUnion {α : Type u} {ι : Sort x} {t : ι → Set α} [Countable ι] (ht : ∀ (i : ι), Set.Countable (t i)) : Set.Countable (⋃ (i : ι), t i)

@[simp]

theorem Set.countable_iUnion_iff {α : Type u} {ι : Sort x} [Countable ι] {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 ∈ s → Set β} (hs : Set.Countable s) : 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) : Set.Countable (⋃₀ s) ↔ ∀ a ∈ s, Set.Countable a

theorem Set.Countable.biUnion {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a ∈ s → Set β} (hs : Set.Countable s) : (∀ (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 : Set.Countable s) : (∀ a ∈ s, Set.Countable a) → Set.Countable (⋃₀ s)

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

@[simp]

theorem Set.countable_union {α : Type u} {s : Set α} {t : Set α} : Set.Countable (s ∪ t) ↔ Set.Countable s ∧ Set.Countable t

theorem Set.Countable.union {α : Type u} {s : Set α} {t : Set α} (hs : Set.Countable s) (ht : Set.Countable t) : Set.Countable (s ∪ t)

theorem Set.Countable.of_diff {α : Type u} {s : Set α} {t : Set α} (h : Set.Countable (s \ t)) (ht : Set.Countable t) : Set.Countable s

@[simp]

theorem Set.countable_insert {α : Type u} {s : Set α} {a : α} : Set.Countable (insert a s) ↔ Set.Countable s

theorem Set.Countable.insert {α : Type u} {s : Set α} (a : α) (h : Set.Countable s) : Set.Countable (insert a s)

theorem Set.Finite.countable {α : Type u} {s : Set α} (hs : Set.Finite s) : Set.Countable s

theorem Set.Countable.of_subsingleton {α : Type u} [Subsingleton α] (s : Set α) : Set.Countable s

theorem Set.Subsingleton.countable {α : Type u} {s : Set α} (hs : Set.Subsingleton s) : Set.Countable s

theorem Set.countable_isTop (α : Type u_1) [PartialOrder α] : Set.Countable {x : α | IsTop x}

theorem Set.countable_isBot (α : Type u_1) [PartialOrder α] : Set.Countable {x : α | IsBot x}

theorem Set.countable_setOf_finite_subset {α : Type u} {s : Set α} (hs : Set.Countable s) : Set.Countable {t : Set α | Set.Finite t ∧ t ⊆ s}

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 : α), Set.Countable (s a)) : Set.Countable (Set.pi Set.univ s)

theorem Set.countable_pi {α : Type u} {π : α → Type u_1} [Finite α] {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 : Set.Countable s) (ht : Set.Countable t) : Set.Countable (s ×ˢ t)

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

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 s) : 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 : Finset α) : Set.Countable ↑s