Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.nullMeasurable_image_of_fderivWithin
Modification history
2025-06-25 15:49
Mathlib/MeasureTheory/Function/Jacobian.lean
feat: weaken assumption to `NullMeasurableSet` in some results on change of variables in integrals (#26362)
Added
MeasureTheory.nullMeasurable_image_of_fderivWithin
View on Github →