measurableSet_biUnion — Mathlib

English

If s is a finite set of indices, and each f(b) is measurable for b ∈ s, then the union over b in s of f(b) is measurable.

Русский

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

LaTeX

$$$\text{Finset}(s).measurableSet\_biUnion$$$

Lean4

theorem measurableSet_biUnion {f : β → Set α} (s : Finset β) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋃ b ∈ s, f b) :=
  s.finite_toSet.measurableSet_biUnion h

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