eventuallyEq_iInter — Mathlib

English

If s is finite and for all i ∈ s we have s(i) =^l t(i), then the intersections are equal along l: ⋂_{i∈s} s(i) =^l ⋂_{i∈s} t(i).

Русский

Если s конечное и для всех i∈s выполнено s(i) =^l t(i), то пересечения равны вдоль l: ⋂_{i∈s} s(i) =^l ⋂_{i∈s} t(i).

LaTeX

$$$[s \text{ finite}]\quad (\forall i \in s, s(i) =^l t(i)) \Rightarrow (\bigcap_{i \in s} s(i) =^l \bigcap_{i \in s} t(i)).$$$

Lean4

theorem _root_.Set.Finite.eventuallyEq_iInter {ι : 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.biInter hs fun i hi ↦ (heq i hi).le).antisymm <| .biInter hs fun i hi ↦ (heq i hi).symm.le

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