countable_bInter — Mathlib

English

If S is countable and s_i ≤^l t_i for all i ∈ S, then ⋂_{i∈S} s_i ≤^l ⋂_{i∈S} t_i.

Русский

Если S счетно, и для каждого i∈S выполнено s_i ⊆ t_i относительно l, то пересечение по i∈S сохраняет вложение относительно l.

LaTeX

$$$\\forall S \\subseteq ι,\\ S\\text{ Countable} \\Rightarrow (\\forall i∈S, s(i) ≤^l t(i)) \\Rightarrow (\\bigcap_{i∈S} s(i)) ≤^l (\\bigcap_{i∈S} 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 ‹_› :=
  by
  simp only [biInter_eq_iInter]
  haveI := hS.toEncodable
  exact EventuallyLE.countable_iInter fun i => h i i.2

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