Theorem MeasureTheory.Measure.lintegral_bind_le

Modification history

2026-08-26 08:21
Mathlib/MeasureTheory/Measure/GiryMonad.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified MeasureTheory.Measure.lintegral_bind_leView on Github →
2025-04-06 07:30
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(MeasureTheory): add `lintegral_bind_le` etc (#23716) …
Added MeasureTheory.Measure.lintegral_bind_leView on Github →