eventuallyEq_iUnion — Mathlib

English

Let s be a finite set of indices. If for all i in 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 (\bigcup_{i \in s} f(i) =^l \bigcup_{i \in s} g(i)).$$$

Lean4

theorem _root_.Finset.eventuallyEq_iUnion {ι : Type*} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) :
    (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i) :=
  .biUnion s.finite_toSet heq

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