restrict_add_restrict_compl — Mathlib

English

If s is measurable, then μ restricted to s plus μ restricted to the complement of s equals μ.

Русский

Если s измеримо, то μ ограниченное на s плюс μ ограниченное на дополнение s равно μ.

LaTeX

$$$MeasurableSet\,s \implies \mu\restriction s + \mu\restriction s^c = \mu$$$

Lean4

@[simp]
theorem restrict_add_restrict_compl (hs : MeasurableSet s) : μ.restrict s + μ.restrict sᶜ = μ := by
  rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self, restrict_univ]

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