Commit 2026-02-04 08:49 9a038489

View on Github →

feat(Measure): add gcongr lemmas (#34723)

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.measure_mono_both

added theorem MeasureTheory.Measure.measure_mono_left