Theorem MeasureTheory.Measure.le_join_apply

Modification history

2025-04-06 07:30
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(MeasureTheory): add `lintegral_bind_le` etc (#23716) …
Added MeasureTheory.Measure.le_join_applyView on Github →