measure_union' — Mathlib

English

A variant of additivity: if s1 is measurable, then μ(s1 ∪ s2) = μ(s1) + μ(s2).

Русский

Вариант аддитивности: если s1 измеримо, то μ(s1 ∪ s2) = μ(s1) + μ(s2).

LaTeX

$$$$\\mathrm{MeasurableSet}(s_1) \\Rightarrow \\mu(s_1\\cup s_2) = \\mu(s_1) + \\mu(s_2).$$$$

Lean4

theorem measure_union' (hd : Disjoint s₁ s₂) (h : MeasurableSet s₁) : μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
  measure_union₀' h.nullMeasurableSet hd.aedisjoint

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