# Documentation

Mathlib.SetTheory.Cardinal.CountableCover

# Cardinality of a set with a countable cover #

Assume that a set t is eventually covered by a countable family of sets, all with cardinality ≤ a. Then t itself has cardinality at most a. This is proved in Cardinal.mk_subtype_le_of_countable_eventually_mem.

Versions are also given when t = univ, and with = a instead of ≤ a.

theorem Cardinal.mk_subtype_le_of_countable_eventually_mem_aux {α : Type u} {ι : Type u} {a : Cardinal.{u}} [] {f : ιSet α} {l : } [] {t : Set α} (ht : ∀ (x : α), x t∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk ↑(f i) a) :
a

If a set t is eventually covered by a countable family of sets, all with cardinality at most a, then the cardinality of t is also bounded by a. Supersed by mk_le_of_countable_eventually_mem which does not assume that the indexing set lives in the same universe.

theorem Cardinal.mk_subtype_le_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal.{u}} [] {f : ιSet α} {l : } [] {t : Set α} (ht : ∀ (x : α), x t∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk ↑(f i) a) :
a

If a set t is eventually covered by a countable family of sets, all with cardinality at most a, then the cardinality of t is also bounded by a.

theorem Cardinal.mk_le_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal.{u}} [] {f : ιSet α} {l : } [] (ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk ↑(f i) a) :
a

If a space is eventually covered by a countable family of sets, all with cardinality at most a, then the cardinality of the space is also bounded by a.

theorem Cardinal.mk_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal.{u}} [] {f : ιSet α} {l : } [] (ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk ↑(f i) = a) :
= a

If a space is eventually covered by a countable family of sets, all with cardinality a, then the cardinality of the space is also a.