countable_iUnion — Mathlib

English

If (s_i ≤ᶠ[l] t_i) for all i and ι is countable, then the union over i of s_i is eventually contained in the union of t_i: ⋃ i s_i ≤ᶠ[l] ⋃ i t_i.

Русский

Если для всех i выполняется s_i ≤ᶠ[l] t_i и ι счётно, то объединение по i сохраняет отношение: ⋃ i s_i ≤ᶠ[l] ⋃ i t_i.

LaTeX

$$$\\bigcup_i s_i \\leq^{\\!\\mathrm{f}}_l \\bigcup_i t_i$$$

Lean4

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

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