English
If s is a finite set of indices and for all i in s we have f(i) ≤^l g(i), then the union over i in s of f(i) is ≤^l the union over i in s of g(i).
Русский
Если s—конечное подмножество индексов и для всех i∈s выполняется f(i) ≤^l g(i), то объединение по i∈s f(i) ≤^l объединение по i∈s g(i).
LaTeX
$$$[s \text{ finite}]\quad (\forall i \in s, f(i) \le^l g(i)) \Rightarrow \left(\bigcup_{i \in s} f(i) \le^l \bigcup_{i \in s} g(i)\right).$$$
Lean4
theorem _root_.Set.Finite.eventuallyLE_iUnion {ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α}
(hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i) :=
by
have := hs.to_subtype
rw [biUnion_eq_iUnion, biUnion_eq_iUnion]
exact .iUnion fun i ↦ hle i.1 i.2
