Commit 2024-04-29 15:11 194da0f9

View on Github →

feat: absolute continuity of a sum of measures (#12441)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.absolutelyContinuous_sum_left

added theorem MeasureTheory.Measure.absolutelyContinuous_sum_right