measure_union — Mathlib

English

If s1 and s2 are disjoint and s2 is measurable, the measure is additive on their union: μ(s1 ∪ s2) = μ(s1) + μ(s2).

Русский

Если s1 и s2 взаимно пререкаются и s2 измеримо, мера суммируется на объединении: μ(s1 ∪ s2) = μ(s1) + μ(s2).

LaTeX

$$$$\\mathrm{Disjoint}(s_1,s_2) \\Rightarrow \\mathrm{MeasurableSet}(s_2) \\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

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