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}} [Countable ι] {f : ιSet α} {l : Filter ι} [l.NeBot] {t : Set α} (ht : xt, ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk (f i) 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. Superseded 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}} [Countable ι] {f : ιSet α} {l : Filter ι} [l.NeBot] {t : Set α} (ht : xt, ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk (f i) 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}} [Countable ι] {f : ιSet α} {l : Filter ι} [l.NeBot] (ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk (f i) 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}} [Countable ι] {f : ιSet α} {l : Filter ι} [l.NeBot] (ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x f i) (h'f : ∀ (i : ι), Cardinal.mk (f i) = 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.