restrict_union_add_inter — Mathlib

English

For measurable S, μ|_{S∪T} + μ|_{S∩T} = μ|_S + μ|_T for all T.

Русский

Для измеримого S: μ|_{S∪T} + μ|_{S∩T} = μ|_S + μ|_T для любого T.

LaTeX

$$$ (\mu.restrict (S \cup T)) + (\mu.restrict (S \cap T)) = (\mu.restrict S) + (\mu.restrict T) $$$

Lean4

theorem restrict_union_add_inter (s : Set α) (ht : MeasurableSet t) :
    μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t :=
  restrict_union_add_inter₀ s ht.nullMeasurableSet

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