instCountableInterFilter — Mathlib

English

The almost-everywhere filter ae μ is closed under countable intersections: if A_n ∈ ae μ for all n, then ∩_n A_n ∈ ae μ.

Русский

Фильтр almost everywhere ae μ замкнут относительно счетных пересечений: если A_n ∈ ae μ для всех n, то ∩_n A_n ∈ ae μ.

LaTeX

$$$\text{CountableInterFilter} (\mathrm{ae}\,\mu)$$$

Lean4

instance instCountableInterFilter : CountableInterFilter (ae μ) := by unfold ae; infer_instance

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