sUnion — Mathlib

English

Union of a countable collection of sets, each BaireMeasurableSet, is BaireMeasurableSet.

Русский

Объединение счётной коллекции множеств, каждое из которых Баирово измеримо, сохраняет Баирову измеримость.

LaTeX

$$$$ \forall s : \text{Set}(\text{Set } α),\; s.\Countable \Rightarrow (\forall t \in s, \mathrm{BaireMeasurableSet}(t)) \Rightarrow \mathrm{BaireMeasurableSet}(\bigcup s). $$$$

Lean4

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

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