Mathlib Changelog
v4
Changelog
About
Github
Theorem
Measurable.ennreal_sigmaFinite_induction
Modification history
2025-03-29 00:17
Mathlib/MeasureTheory/Function/SimpleFunc.lean
chore: review of induction branch names (#23358) …
Modified
Measurable.ennreal_sigmaFinite_induction
View on Github →
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 →