Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positive

∀ {α : 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

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

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpace