countable_iInter — Mathlib

English

If each s_i ≤^l t_i for i ∈ ι with ι countable, then ⋂_i s_i ≤^l ⋂_i t_i.

Русский

Если каждое s_i вложено в t_i относительно l, для всех i из счетного множества ι, то ⋂_i s_i вложено в ⋂_i t_i относительно l.

LaTeX

$$$\\forall ι\\; [Countable],\\, (s,t: ι \\to Set(α)), (\\forall i, s(i) \\leq^l t(i)) \\Rightarrow (\\bigcap_{i} s(i)) \\leq^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 :=
  (eventually_countable_forall.2 h).mono fun _ hst hs => mem_iInter.2 fun i => hst _ (mem_iInter.1 hs i)

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