iInter — Mathlib

English

Countable intersection of BaireMeasurableSet is BaireMeasurableSet.

Русский

Счётное пересечение Баирово измеримых множеств сохраняет свойство Баирово измеримого.

LaTeX

$$$$ \forall ι, [Countable ι], {s : ι \to Set α}, (h : \forall i, \mathrm{BaireMeasurableSet}(s(i))) \Rightarrow \mathrm{BaireMeasurableSet}(\bigcap_i s(i)). $$$$

Lean4

theorem iInter {ι : Sort*} [Countable ι] {s : ι → Set α} (h : ∀ i, BaireMeasurableSet (s i)) :
    BaireMeasurableSet (⋂ i, s i) :=
  MeasurableSet.iInter h

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