Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.SimpleFunc.mk_le_mk
Modification history
2024-11-07 15:53
Mathlib/MeasureTheory/Function/SimpleFunc.lean
feat: induction principle for `ENNReal`-valued measurable functions from a sigma-finite space (#17835) …
Added
MeasureTheory.SimpleFunc.mk_le_mk
View on Github →