sUnion — Mathlib

English

Countable union of a collection of sets is measurable, provided each set is measurable.

Русский

Счётное объединение коллекции множеств измеримо при условии измеримости каждого множества.

LaTeX

$$$[Countable\ ι] \; (\forall t \in \mathcal S, \MeasurableSet(t)) \Rightarrow \MeasurableSet\left(\bigcup \mathcal S\right)$$$

Lean4

protected theorem sUnion {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋃₀ s) :=
  by
  rw [sUnion_eq_biUnion]
  exact .biUnion hs h

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