Commit 2023-05-22 18:01 2b47ec0c

View on Github →

chore: forward-port leanprover-community/mathlib#18983 (#4001)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.toOuterMeasure_top

added theorem MeasureTheory.OuterMeasure.toMeasure_top

Modified Mathlib/MeasureTheory/Measure/OuterMeasure.lean

added theorem MeasureTheory.OuterMeasure.boundedBy_top

added theorem MeasureTheory.OuterMeasure.boundedBy_zero

added theorem MeasureTheory.OuterMeasure.trim_top

added theorem MeasureTheory.extend_top