measure_union_add_inter₀ — Mathlib

English

If t is null-measurable with respect to μ, then for every s the equality μ(s ∪ t) + μ(s ∩ t) = μ(s) + μ(t) holds.

Русский

Если t является нулево измеримым относительно μ, то для любого s выполняется равенство μ(s ∪ t) + μ(s ∩ t) = μ(s) + μ(t).

LaTeX

$$$\mathrm{NullMeasurableSet}(t,\mu) \Rightarrow \forall s,\; \mu(s \cup t) + \mu(s \cap t) = \mu(s) + \mu(t).$$$

Lean4

theorem measure_union_add_inter₀ (s : Set α) (ht : NullMeasurableSet t μ) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t := by
  rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ← measure_inter_add_diff₀ s ht,
    add_comm, ← add_assoc, add_right_comm]

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