Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero

Deprecated since 2026-06-03Use MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero instead.

∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  MeasurableSet A → MeasurableSet B → v (B \ A) = 0 → v (A \ B) + v B = v A

Alias of MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpaceT2Space