Commit 2024-05-13 13:38 cd37814c

View on Github →

feat: define MeasureTheory.OuterMeasureClass (#12855)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

deleted theorem MeasureTheory.OuterMeasure.measureOf_eq_coe

deleted structure MeasureTheory.OuterMeasure

Created Mathlib/MeasureTheory/OuterMeasure/Defs.lean

added theorem MeasureTheory.OuterMeasure.measureOf_eq_coe

added structure MeasureTheory.OuterMeasure