Theorem MeasureTheory.Measure.bind_const

Modification history

2024-10-13 09:56

Mathlib/MeasureTheory/Measure/GiryMonad.lean

feat(MeasureTheory): two lemmas about `Measure.bind` (#17630) …

Added MeasureTheory.Measure.bind_const View on Github →