Theorems · Theorem · logic and foundations

Cardinal.mk_subtype_le_of_countable_eventually_mem

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

Defined in

Mathlib.SetTheory.Cardinal.CountableCover

Cited by

1 results in Mathlib

Foundations

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

Assumes

CountableFilter.NeBot