English
If a space is eventually covered by a countable family of sets, each of cardinality at most a, then the space has cardinality at most a.
Русский
Если пространство в итоге покрывается счётной семейством множеств, каждое из которых имеет кардинальность не более a, то кардинальность пространства не превосходит a.
LaTeX
$$$\#\alpha \le a$ given (∃ l, ∀ x, ∀^\infty i ∈ l, x ∈ f(i)) \land (∀ i, \#(f(i)) ≤ a)$$
Lean4
/-- 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 mk_subtype_le_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal} [Countable ι] {f : ι → Set α}
{l : Filter ι} [NeBot l] {t : Set α} (ht : ∀ x ∈ t, ∀ᶠ i in l, x ∈ f i) (h'f : ∀ i, #(f i) ≤ a) : #t ≤ a :=
by
let g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (ULift.down ⁻¹' ·) ∘ f ∘ ULift.down
suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
let l' : Filter (ULift.{u} ι) := Filter.map ULift.up l
have : NeBot l' := map_neBot
apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
· intro x hx
simpa only [Function.comp_apply, mem_preimage, eventually_map] using ht _ hx
· intro i
simpa [g] using h'f i.down
