Theorem MeasureTheory.Measure.join_map_dirac

Modification history

2024-10-13 09:56
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(MeasureTheory): two lemmas about `Measure.bind` (#17630) …
Modified MeasureTheory.Measure.join_map_diracView on Github →
2023-05-22 03:13
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat: port MeasureTheory.Measure.GiryMonad (#4103)
Added MeasureTheory.Measure.join_map_diracView on Github →