Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-12-09 17:36
efe18d5d
View on Github →
feat(measure_theory/interval_integral): continuous implies interval_integrable (
#5288
)
Estimated changes
Modified
src/measure_theory/interval_integral.lean
added
theorem
continuous.interval_integrable
added
theorem
continuous_on.interval_integrable