Theorems · Theorem · logic and foundations

Cardinal.mk_of_countable_eventually_mem

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

Defined in

Mathlib.SetTheory.Cardinal.CountableCover

Cited by

1 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableFilter.NeBot