English
Let l be a filter on α with CountableInterFilter. If S is a countable subset of ι and, for each i ∈ S, s_i ⊆_l t_i (i.e., s_i ≤^l t_i eventually), then ⋃_{i∈S} s_i ⊆_l ⋃_{i∈S} t_i.
Русский
Пусть l — фильтр на α с свойством счетного пересечения. Пусть S счетно по ι и для каждого i ∈ S выполнено s_i ⊆_l t_i. Тогда объединение ⋃_{i∈S} s_i содержится в ⋃_{i∈S} t_i относительно l (в смысле включения почти наверно).
LaTeX
$$$\\forall S \\subseteq ι,\\, S\\text{ счетно},\\ \\forall s,t:\\(i\\mapsto Set(α))\\, (\\forall i∈S,\\, s(i) \\leq^l t(i)) \\Rightarrow (\\bigcup_{i∈S} s(i)) \\leq^l (\\bigcup_{i∈S} 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 ‹_› :=
by
simp only [biUnion_eq_iUnion]
haveI := hS.toEncodable
exact EventuallyLE.countable_iUnion fun i => h i i.2
