restrict_union_add_inter₀ — Mathlib

English

If s is measurable, then μ|_{s∪t} + μ|_{s∩t} = μ|_s + μ|_t for any 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 : NullMeasurableSet t μ) :
    μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t := by
  rw [← restrict_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
    restrict_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]

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