Commit 2026-09-24 11:48 0c82d69c

View on Github →

chore(MeasureTheory): using ENNReal instead of NNReal (#42261) This PR removes coercions in some files in MeasureTheory (i.e. working directly with ENNReal instead of working with NNReal and coercing), focusing on MeasureTheory.Covering.Differentiation. The resulting files are a bit shorter and a more legible.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

modified theorem VitaliFamily.exists_measurable_supersets_limRatio

modified theorem VitaliFamily.le_mul_withDensity

modified theorem VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt

modified theorem VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas

modified theorem VitaliFamily.null_of_frequently_le_of_frequently_ge

modified theorem VitaliFamily.withDensity_le_mul

Modified Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

modified theorem ENNReal.aemeasurable_of_exist_almost_disjoint_supersets

modified theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

added theorem MeasureTheory.Measure.isLocallyFiniteMeasure_smul