nullMeasurableSet_biUnion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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