nullMeasurableSet_sUnion — Mathlib

English

If s is finite and every t in s is null-measurable, then the sUnion (the union of all elements of s) is null-measurable.

Русский

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

LaTeX

$$$s\text{ finite} \Rightarrow (\forall t\in s, \mathrm{NullMeasurableSet}(t,\mu)) \Rightarrow \mathrm{NullMeasurableSet}(\bigcup s,\mu).$$$

Lean4

theorem _root_.Set.Finite.nullMeasurableSet_sUnion {s : Set (Set α)} (hs : s.Finite)
    (h : ∀ t ∈ s, NullMeasurableSet t μ) : NullMeasurableSet (⋃₀ s) μ :=
  Finite.measurableSet_sUnion hs h

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