Theorem MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iff

Modification history

2026-09-03 15:14
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
chore(MeasureTheory/VectorMeasure): split long file Basic.lean (#43271) …
Modified MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iffView on Github →
2025-06-23 08:19
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition (#23500) …
Added MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iffView on Github →