English
If a set t is eventually covered by a countable family of sets f_i, each with cardinality at most a, then the cardinality of t is at most a.
Русский
Если множество t в итоге покрывается счётной семейством множеств f_i, каждое из которых имеет кардинальность не более a, то кардинальность t не превышает a.
LaTeX
$$$\#t \le a$ given (∀ x ∈ t, ∀^\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`.
Superseded by `mk_le_of_countable_eventually_mem` which does not assume
that the indexing set lives in the same universe. -/
theorem mk_subtype_le_of_countable_eventually_mem_aux {α ι : Type u} {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
rcases lt_or_ge a ℵ₀ with ha | ha
· obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
rcases B.exists with ⟨i, hi⟩
have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
let u : Finset α := (f i).toFinset
have I1 : s.card ≤ u.card :=
by
have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
exact Finset.card_le_card this
have I2 : (u.card : Cardinal) ≤ n := by convert h'f i; simp only [u, Set.toFinset_card, mk_fintype]
exact
I1.trans
(Nat.cast_le.1 I2)
-- case `a` infinite:
· have : t ⊆ ⋃ i, f i := by
intro x hx
obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
exact mem_iUnion_of_mem i hi
calc
#t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
_ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
_ ≤ sum (fun _ ↦ a) := (sum_le_sum _ _ h'f)
_ = #ι * a := by simp
_ ≤ ℵ₀ * a := (mul_le_mul_right' mk_le_aleph0 a)
_ = a := aleph0_mul_eq ha
