restrict_union' — Mathlib

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]

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