MeasureSpace instance on Subtype

Stream: mathlib4

[Yury G. Kudryashov]

Currently, we have a MeasureSpace instance on Subtype _, introduced in !3#16708. I'm not sure if this should be an instance: while it works fine for subsets of positive measure, some sets of zero measure have natural lower-dimensional volume.

[Yury G. Kudryashov]

@Alex J. Best @Rémy Degenne @Sebastien Gouezel :up:

[Sebastien Gouezel]

I agree with you that's is debatable (for instance, the real line in the complex plane has a more natural measure than the zero measure). It's probably safer to have it as a definition, which one can register locally as an instance when needed.

[Rémy Degenne]

That sounds like a good reason to not have it as an instance :+1:

[Eric Wieser]

#8381 removes it