Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-16 14:39
bf0bc236
View on Github →
feat: lemmas about Lebesgue integral (
#7681
)
From the Sobolev project
Estimated changes
Modified
Mathlib/Data/Real/ENNReal.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
added
theorem
MeasureTheory.lintegral_mono_fn'
added
theorem
MeasureTheory.lintegral_mono_fn
added
theorem
MeasureTheory.lintegral_of_isEmpty