sInter — Mathlib

English

Countable intersection of sets in a countable family is BaireMeasurableSet.

Русский

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

LaTeX

$$$$ \forall {s : Set(Set α)}, (hs : s.Countable) (h : \forall t \in s, \mathrm{BaireMeasurableSet}(t)) \Rightarrow \mathrm{BaireMeasurableSet}(\bigcap s). $$$$

Lean4

theorem sInter {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, BaireMeasurableSet t) : BaireMeasurableSet (⋂₀ s) :=
  MeasurableSet.sInter hs h

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