restrict_inter_add_diff₀ — Mathlib

English

For a null-measurable 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 : NullMeasurableSet t μ) :
    μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s :=
  by
  ext1 u hu
  simp only [add_apply, restrict_apply hu, ← inter_assoc, diff_eq]
  exact measure_inter_add_diff₀ (u ∩ s) ht

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