English
Let l be a filter on α with the countable intersection property. If (s_i) and (t_i) are families of subsets of α indexed by a countable index set ι, and for every i we have s_i =_l t_i, then the unions ⋃_i s_i and ⋃_i t_i are also equal modulo l: ⋃_i s_i =_l ⋃_i t_i.
Русский
Пусть l — фильтр на α, обладающий свойством счетного пересечения. Пусть s_i и t_i — семейства подмножеств α, индексируемые счетной множеством ι, и для каждого i выполняется s_i =_l t_i. Тогда их объединения по i: ⋃_i s_i и ⋃_i t_i равны «модульно» относительно l.
LaTeX
$$$\\forall ι \\; [\\,\\text{Countable}] \\, (s,t: ι \\to \\mathcal{P}(α)) \, (\\forall i, s(i) =_l t(i)) \\Longrightarrow (\\bigcup_{i} s(i)) =_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 :=
(EventuallyLE.countable_iUnion fun i => (h i).le).antisymm (EventuallyLE.countable_iUnion fun i => (h i).symm.le)
