Theorem MeasureTheory.Measure.bind_zero_right'

Modification history

2025-04-08 13:38

Mathlib/MeasureTheory/Measure/GiryMonad.lean

feat(GiryMonad): use `AEMeasurable` (#23754) …

Modified MeasureTheory.Measure.bind_zero_right'View on Github →

2023-05-22 03:13

Mathlib/MeasureTheory/Measure/GiryMonad.lean

feat: port MeasureTheory.Measure.GiryMonad (#4103)

Added MeasureTheory.Measure.bind_zero_right'View on Github →