restrict_union — Mathlib

English

If s and t are disjoint and t is measurable, then μ restricted to s ∪ t equals μ restricted to s plus μ restricted to t.

Русский

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

LaTeX

$$$Disjoint\,s\,t \land MeasurableSet\,t \implies \mu\restriction (s \cup t) = \mu\restriction s + \mu\restriction t$$$

Lean4

theorem restrict_union (h : Disjoint s t) (ht : MeasurableSet t) : μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
  restrict_union₀ h.aedisjoint ht.nullMeasurableSet

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