measurableSet_sUnion — Mathlib

English

If s is finite, the supremum union of sets in s is measurable provided each set is measurable.

Русский

Если s конечно, объединение объединений множества s измеримо при условии, что каждое множество измеримо.

LaTeX

$$$[s.Finite] (\forall t \in s, \MeasurableSet t) \Rightarrow \MeasurableSet\left(\bigcup\!_{t \in s} t\right)$$$

Lean4

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

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