Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.Measure.lintegral_bind_le
Modification history
2025-04-06 07:30
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(MeasureTheory): add `lintegral_bind_le` etc (#23716) …
Added
MeasureTheory.Measure.lintegral_bind_le
View on Github →