Theorem MeasureTheory.Measure.join_dirac

Modification history

2025-04-08 13:38
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(GiryMonad): use `AEMeasurable` (#23754) …
Modified MeasureTheory.Measure.join_diracView on Github →
2023-05-22 03:13
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat: port MeasureTheory.Measure.GiryMonad (#4103)
Added MeasureTheory.Measure.join_diracView on Github →