measure_union₀' — Mathlib

English

If s is null-measurable with respect to μ and s is almost disjoint from t, then μ(s ∪ t) = μ(s) + μ(t).

Русский

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

LaTeX

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

Lean4

theorem measure_union₀' (hs : NullMeasurableSet s μ) (hd : AEDisjoint μ s t) : μ (s ∪ t) = μ s + μ t := by
  rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]

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