countable_bInter — Mathlib

English

If s_i =^l t_i for all i in ι, 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_bInter {ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α}
    (h : ∀ i hi, s i hi =ᶠ[l] t i hi) : ⋂ i ∈ S, s i ‹_› =ᶠ[l] ⋂ i ∈ S, t i ‹_› :=
  (EventuallyLE.countable_bInter hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.countable_bInter hS fun i hi => (h i hi).symm.le)

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