restrict_add_restrict_compl — Mathlib

English

Let i be measurable. Then restricting v to i and to its complement i^c yields the whole measure: v|i + v|i^c = v.

Русский

Пусть i измеримо. Тогда ограничение v до i и до комплемента i^c суммарно даёт исходную меру: v|i + v|i^c = v.

LaTeX

$$$ v \\restriction i + v \\restriction i^{c} = v $$$

Lean4

@[simp]
theorem restrict_add_restrict_compl (hi : MeasurableSet i) : v.restrict i + v.restrict iᶜ = v :=
  by
  ext A hA
  rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA, ← of_union _ (hA.inter hi) (hA.inter hi.compl)]
  · simp
  · exact disjoint_compl_right.inter_right' A |>.inter_left' A

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