restrict_inter_add_diff — Mathlib

English

For any sets s,t with t null-measurable, μ|_{s∪t} + μ|_{s∩t} = μ|_s + μ|_t.

Русский

Для любых множеств s,t с t нулевой измеримости: μ|_{s∪t} + μ|_{s∩t} = μ|_s + μ|_t.

LaTeX

$$$ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t $$$

Lean4

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

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