Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative

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

The symmetric difference of two Hahn decompositions has measure zero.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace