measure_diff' — Mathlib

English

For s ⊂ α and null-measurable t with finite μ(t), μ(s \\ t) = μ(s ∪ t) − μ(t).

Русский

Для любых s и нулемеримого t с конечной μ(t) выполняется μ(s \\ t) = μ(s ∪ t) − μ(t).

LaTeX

$$$$ \\mu\\left(s \\setminus t\\right) = \\mu(s \\cup t) - \\mu(t). $$$$

Lean4

theorem measure_diff' (s : Set α) (hm : NullMeasurableSet t μ) (h_fin : μ t ≠ ∞) : μ (s \ t) = μ (s ∪ t) - μ t :=
  ENNReal.eq_sub_of_add_eq h_fin <| by rw [add_comm, measure_add_diff hm, union_comm]

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