nullMeasurableSet_biUnion — Mathlib

English

If s is finite and each f(b) is null-measurable, then the union over b in s of f(b) is null-measurable.

Русский

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

LaTeX

$$$s\text{ finite} \Rightarrow (\forall b, b\in s \rightarrow \mathrm{NullMeasurableSet}(f(b),\mu)) \Rightarrow \mathrm{NullMeasurableSet}(\bigcup_{b\in s} f(b),\mu).$$$

Lean4

theorem _root_.Finset.nullMeasurableSet_biUnion {f : ι → Set α} (s : Finset ι)
    (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : NullMeasurableSet (⋃ b ∈ s, f b) μ :=
  Finset.measurableSet_biUnion s h

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