Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.integral_tsum_of_summable_integral_norm
Modification history
2024-03-04 19:37
Mathlib/MeasureTheory/Integral/Bochner.lean
refactor: move material about the Dominated Convergence Theorem into one file (#11139) …
Modified
MeasureTheory.integral_tsum_of_summable_integral_norm
View on Github →
2024-02-27 15:33
Mathlib/MeasureTheory/Integral/Bochner.lean
feat(MeasureTheory/Integral): hasSum_integral_of_summable_integral_norm (#10614) …
Added
MeasureTheory.integral_tsum_of_summable_integral_norm
View on Github →