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