English
Let l be a filter on α, ι a finite index set, and s,t : ι → Set α. If for every i we have s(i) =^l t(i) (they are equal along l), then the unions are equal along l: ⋃_i s(i) =^l ⋃_i t(i).
Русский
Пусть l — фильтр на α, ι — конечный индексный набор, и s,t : ι → Set α. Если для каждого i выполняется s(i) =^l t(i) (они равны вдоль l), тогда объединения равны вдоль l: ⋃_i s(i) =^l ⋃_i t(i).
LaTeX
$$$[\text{Finite } ι]\quad (\forall i, s(i) =^l t(i)) \Rightarrow (\bigcup_i s(i) =^l \bigcup_i t(i)).$$$
Lean4
protected theorem iUnion [Finite ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : (⋃ i, s i) =ᶠ[l] ⋃ i, t i :=
(EventuallyLE.iUnion fun i ↦ (h i).le).antisymm <| .iUnion fun i ↦ (h i).symm.le
