Theorem MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn

Modification history

2025-06-24 07:54
Mathlib/MeasureTheory/Function/JacobianOneDim.lean
feat: change of variables formula in integrals for monotone functions (#26198) …
Added MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOnView on Github →