Measurable space over probability measures

Stream: Is there code for X?

[Markus de Medeiros]

I'm working on cleaning up a lemma related to the Giry monad over probability spaces. Is there a MeasurableSpace instance for ProbabilityMeasure somewhere that I'm somehow not triggering or is this missing?

mwe:

import Mathlib.MeasureTheory.Measure.GiryMonad
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
noncomputable section
open  ENNReal MeasureTheory MeasureTheory.Measure
variable {α : Type*} [MeasurableSpace α]
#synth MeasurableSpace (Measure α) -- OK
#synth MeasurableSpace { μ : Measure α // IsProbabilityMeasure μ } -- OK
-- #synth MeasurableSpace (ProbabilityMeasure α) -- Fails