Commit 2023-11-13 13:49 022c6839

chore: disable global instance Subtype.measureSpace (#8381) Currently, a subtype of a MeasureSpace has a MeasureSpace instance, obtained by restricting the initial measure. There are however other reasonable constructions, like the normalized restriction for a probability measure, or the subspace measure when restricting to a vector subspace. We disable the global instance Subtype.measureSpace to make these other choices possible, as discussed on Zulip. It turns out that this instance was duplicated in SetCoe.measureSpace, so we delete the other one.