Commit 2023-10-18 06:36 29fc60fc

View on Github →

feat: Prove Measure.add_right_inj for sigma-finite measures (#7727)

Generalizes a lemma from #7713.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.add_left_inj

added theorem MeasureTheory.Measure.add_right_inj

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.Measure.ext_iff'