countable_iInter — Mathlib

English

Let l be a filter on α with CountableInterFilter. If s_i =^l t_i for all i, then ⋂_i s_i =^l ⋂_i t_i.

Русский

Пусть для каждого i выполняется s_i =^l t_i. Тогда пересечение по i равносильно относительно l.

LaTeX

$$$\\forall ι \\; [Countable],\\, (s,t: ι \\to Set(α)), (\\forall i, s(i) =_l t(i)) \\Rightarrow (\\bigcap_{i} s(i)) =_l (\\bigcap_{i} t(i))$$$

Lean4

theorem countable_iInter [Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : ⋂ i, s i =ᶠ[l] ⋂ i, t i :=
  (EventuallyLE.countable_iInter fun i => (h i).le).antisymm (EventuallyLE.countable_iInter fun i => (h i).symm.le)

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