English
If s and t are disjoint and s is measurable, then μ restricted to s ∪ t equals μ restricted to s plus μ restricted to t.
Русский
Если s и t распадаются на непересекающиеся множества и s измеримо, то μ ограничено на s ∪ t равно μ ограничено на s плюс μ ограничено на t.
LaTeX
$$$Disjoint\,s\,t \land MeasurableSet\,s \implies \mu\restriction (s \cup t) = \mu\restriction s + \mu\restriction t$$$
Lean4
theorem restrict_union' (h : Disjoint s t) (hs : MeasurableSet s) : μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=
by rw [union_comm, restrict_union h.symm hs, add_comm]