Theorem MeasureTheory.Measure.bind_dirac_eq_map

Modification history

2024-10-13 09:56
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(MeasureTheory): two lemmas about `Measure.bind` (#17630) …
Added MeasureTheory.Measure.bind_dirac_eq_mapView on Github →