Commit 2024-05-07 03:11 f05781e0

View on Github →

refactor(Measure): improve defeq for ⊤ (#12706) Now (⊤ : Measure α).toOuterMeasure = ⊤ is defeq.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.OuterMeasure.toMeasure_top