MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive

Deprecated since 2026-06-03Use MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positive instead.

∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
        MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v →
          s (symmDiff u v) = 0 → s (u \ v) = 0 ∧ s (v \ u) = 0

Alias of MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positive. If the symmetric difference of two positive sets is a null-set, then so are the differences between the two sets.

Defined in: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Cited by: 0 results in Mathlib
Foundations: Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Realstatement · cited by 25,697
MeasurableSpacestatement · cited by 13,106
MeasurableSetstatement · cited by 3,075
MeasureTheory.VectorMeasurestatement · cited by 451
symmDiffstatement · cited by 236
MeasureTheory.VectorMeasure.restrictstatement · cited by 139
MeasureTheory.SignedMeasurestatement · cited by 108
MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positiveproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.