iUnion — Mathlib

English

Countable union of BaireMeasurableSet remains BaireMeasurableSet.

Русский

Счётное объединение множеств Баирово измеримо.

LaTeX

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

Lean4

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

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