measure_symmDiff_eq — Mathlib

English

For sets s,t,u, μ(s Δ u) ≤ μ(s Δ t) + μ(t Δ u).

Русский

Для множеств s,t,u верно μ(s Δ u) ≤ μ(s Δ t) + μ(t Δ u).

LaTeX

$$$$\\forall s,t,u:\\mathrm Set,\\; \\mu(s\\Delta u) \\le \\mu(s\\Delta t) + \\mu(t\\Delta u).$$$$

Lean4

theorem measure_symmDiff_eq (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
    μ (s ∆ t) = μ (s \ t) + μ (t \ s) := by
  simpa only [symmDiff_def, sup_eq_union] using measure_union₀ (ht.diff hs) disjoint_sdiff_sdiff.aedisjoint

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