MeasureSpace instance on unitInterval

Stream: Is there code for X?

[Eric Wieser]

Is this sane as a global instance?

import Mathlib

open unitInterval

noncomputable instance : MeasureTheory.MeasureSpace I :=
  MeasureTheory.Measure.Subtype.measureSpace

[Eric Wieser]

docs#MeasureTheory.Measure.Subtype.measureSpace suggests that there are other sensible measures for arbitrary subtypes, but is the measure on the unit interval canonical?

[Eric Wieser]

(after all, the "normalized restriction for a probability measure" is the same measure here)

[Anatole Dedecker]

I think this is good, I wouldn’t expect any other canonical measure here.

[Eric Wieser]

(The underlying motivation here is #9487: that PR is a long way from being sorry-free, but I need this instance to even state the result!)

[Yury G. Kudryashov]

I think this is good

[Eric Wieser]

#10452, which includes IsProbabilityMeasure (volume : Measure I)

[Eric Wieser]

Could someone take another look at #10452?

[Yury G. Kudryashov]

Delegated