Commit 2026-06-30 05:06 c7369ee5

View on Github →

feat(MeasureTheory): use IsApply for OuterMeasure (#40945)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Map.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Operations.lean

deleted theorem MeasureTheory.OuterMeasure.add_apply

deleted def MeasureTheory.OuterMeasure.coeFnAddMonoidHom

deleted theorem MeasureTheory.OuterMeasure.coe_add

deleted theorem MeasureTheory.OuterMeasure.coe_smul

deleted theorem MeasureTheory.OuterMeasure.coe_zero

deleted theorem MeasureTheory.OuterMeasure.smul_apply