Mathlib Changelog
v4
Changelog
About
Github
Theorem
VitaliFamily.measure_limRatioMeas_zero
Modification history
2026-04-29 14:11
Mathlib/MeasureTheory/Covering/Differentiation.lean
chore: make argument in `zero_le`/`one_le` implicit (#38148) …
Modified
VitaliFamily.measure_limRatioMeas_zero
View on Github →
2023-06-07 08:40
Mathlib/MeasureTheory/Covering/Differentiation.lean
feat: port MeasureTheory.Covering.Differentiation (#4779)
Added
VitaliFamily.measure_limRatioMeas_zero
View on Github →