eventuallyEq_iUnion — Mathlib

English

If s is finite and for all i ∈ s we have f(i) =^l g(i), then the unions are equal along l: ⋃_{i∈s} f(i) =^l ⋃_{i∈s} g(i).

Русский

Если s конечное и для каждого i∈s выполняется f(i) =^l g(i), то объединения равны вдоль l: ⋃_{i∈s} f(i) =^l ⋃_{i∈s} g(i).

LaTeX

$$$[s \text{ finite}]\quad (\forall i \in s, f(i) =^l g(i)) \Rightarrow \left(\bigcup_{i \in s} f(i) =^l \bigcup_{i \in s} g(i)\right).$$$

Lean4

theorem _root_.Set.Finite.eventuallyEq_iUnion {ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α}
    (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i) :=
  (EventuallyLE.biUnion hs fun i hi ↦ (heq i hi).le).antisymm <| .biUnion hs fun i hi ↦ (heq i hi).symm.le

Похожие утверждения