measurableSet_biUnion — Mathlib

English

If s is finite, the union over b ∈ s of f(b) is measurable provided each f(b) is measurable.

Русский

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

LaTeX

$$$[s.Finite] \; (\forall b \in s, \MeasurableSet(f(b))) \Rightarrow \MeasurableSet(\bigcup_{b \in s} f(b))$$$

Lean4

theorem measurableSet_biUnion {f : β → Set α} {s : Set β} (hs : s.Finite) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋃ b ∈ s, f b) :=
  .biUnion hs.countable h

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