measure_union₀ — Mathlib

English

If t is null-measurable and s and t are almost everywhere disjoint, then μ(s ∪ t) = μ(s) + μ(t).

Русский

Если t нулево измеримо и s и t почти нигде не пересекаются, то μ(s ∪ t) = μ(s) + μ(t).

LaTeX

$$$\mathrm{NullMeasurableSet}(t,\mu) \Rightarrow \mathrm{AEDisjoint}(\mu, s, t) \Rightarrow \mu(s \cup t) = \mu(s) + \mu(t).$$$

Lean4

theorem measure_union₀ (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) : μ (s ∪ t) = μ s + μ t := by
  rw [← measure_union_add_inter₀ s ht, hd, add_zero]

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