cardinal_iUnion — Mathlib

English

If hic: #ι < c and for all i, s_i ≤ᶠ[l] t_i, then ⋃ i, s_i ≤ᶠ[l] ⋃ i, t_i.

Русский

Пусть #ι < c и для всех i выполняется s_i ≤ᶠ[l] t_i; тогда ⋃ i s_i ≤ᶠ[l] ⋃ i t_i.

LaTeX

$$$#ι < c \\rightarrow (\\forall i, s_i \\le^l_{\\mathrm{Eventually}} t_i) \\rightarrow \\bigcup_i s_i \\le^l_{\\mathrm{Eventually}} \\bigcup_i t_i$$$

Lean4

theorem cardinal_iUnion {s t : ι → Set α} (hic : #ι < c) (h : ∀ i, s i ≤ᶠ[l] t i) : ⋃ i, s i ≤ᶠ[l] ⋃ i, t i :=
  ((eventually_cardinal_forall hic).2 h).mono fun _ hst hs => mem_iUnion.2 <| (mem_iUnion.1 hs).imp hst

Похожие утверждения