iInter — Mathlib

English

Let l be a filter on α and ι a finite index set. If for every i we have s(i) =^l t(i), then the intersections are equal along l: ⋂_i s(i) =^l ⋂_i t(i).

Русский

Пусть l — фильтр на α и ι конечен. Если для каждого i выполняется s(i) =^l t(i), тогда пересечения равны вдоль l: ⋂_i s(i) =^l ⋂_i t(i).

LaTeX

$$$[\text{Finite } ι]\quad (\forall i, s(i) =^l t(i)) \Rightarrow (\bigcap_i s(i) =^l \bigcap_i t(i)).$$$

Lean4

protected theorem iInter [Finite ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : (⋂ i, s i) =ᶠ[l] ⋂ i, t i :=
  (EventuallyLE.iInter fun i ↦ (h i).le).antisymm <| .iInter fun i ↦ (h i).symm.le

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