measure_union_add_inter — Mathlib

English

For null-measurable sets s and t, μ(s Δ t) = μ(s\\t) + μ(t\\s).

Русский

Для нулевой измеримости множеств s и t верно μ(s Δ t) = μ(s\\t) + μ(t\\s).

LaTeX

$$$$\\forall s,t:\\mathrm Set,\\; \\mathrm{NullMeasurableSet}(s,\\mu) \\rightarrow \\mathrm{NullMeasurableSet}(t,\\mu) \\rightarrow \\mu(s\\Delta t) = \\mu(s\\setminus t) + \\mu(t\\setminus s).$$$$

Lean4

theorem measure_union_add_inter (s : Set α) (ht : MeasurableSet t) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t :=
  by
  rw [← measure_inter_add_diff (s ∪ t) ht, Set.union_inter_cancel_right, union_diff_right, ←
    measure_inter_add_diff s ht]
  ac_rfl

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