LeanPool.QuasiBorelSpaces.MeasureTheory.Instances

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.Instances.

@[implicit_reducible]

instance MeasureTheory.instMeasurableSpacePEmptyLeanPool : MeasurableSpace PEmpty.{u_1 + 1}

Equations

• MeasureTheory.instMeasurableSpacePEmptyLeanPool = ⊤