Mathlib Changelog
v4
Changelog
About
Github
Theorem
Measurable.ennreal_sigmaFinite_induction
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
Measurable.ennreal_sigmaFinite_induction
View on Github →