English
Let l be a filter on α and ι a finite index set. If for every i in ι the set s(i) is eventually a subset of t(i) along l, then the union over i of s(i) is eventually a subset of the union over i of t(i).
Русский
Пусть l — фильтр на α, ι — конечный индексный набор. Если для каждого i ∈ ι множество s(i) вскоре включено в t(i) вдоль l, тогда объединение ⋃_i s(i) вскоре включено в ⋃_i t(i) вдоль l.
LaTeX
$$$ [\text{Finite } \iota]\quad (\forall i, s(i) \le^l t(i)) \Rightarrow (\bigcup_i s(i) \le^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 :=
(eventually_all.2 h).mono fun _x hx hx' ↦
let ⟨i, hi⟩ := mem_iUnion.1 hx';
mem_iUnion.2 ⟨i, hx i hi⟩
