English
Let l be a filter on α with CountableInterFilter. If s_i =^l t_i for every i in ι, then ⋂_i s_i =^l ⋂_i t_i.
Русский
Пусть l — фильтр на α с CountableInterFilter. Если для всех i выполняется s_i =^l t_i, то пересечение по i: ⋂_i s_i равно ⋂_i t_i модульно относительно l.
LaTeX
$$$\\forall ι\\; [Countable]\\, (s,t: ι \\to Set(α)), (\\forall i, s(i) =_l t(i)) \\Rightarrow (\\bigcap_{i} s(i)) =_l (\\bigcap_{i} t(i))$$$
Lean4
theorem countable_bUnion {ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α}
(h : ∀ i hi, s i hi =ᶠ[l] t i hi) : ⋃ i ∈ S, s i ‹_› =ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
(EventuallyLE.countable_bUnion hS fun i hi => (h i hi).le).antisymm
(EventuallyLE.countable_bUnion hS fun i hi => (h i hi).symm.le)
