Theorem MeasureTheory.Measure.measurable_bind'

Modification history

2025-02-15 16:50

Mathlib/MeasureTheory/Measure/GiryMonad.lean

chore: make MeasurableSpace arguments implicit (#21907) …

Modified MeasureTheory.Measure.measurable_bind'View on Github →

2023-05-22 03:13

Mathlib/MeasureTheory/Measure/GiryMonad.lean

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

Added MeasureTheory.Measure.measurable_bind'View on Github →