Countable separating family of sets

Stream: maths

[Felix Weilacher]

I'd like to add a type class to abbreviate [HasCountableSeparatingOn X MeasurableSet univ], where X is a type with a MeasurableSpace instance. Is there a name for this? I was thinking [CountablySeparated X].

[Yury G. Kudryashov]

Will it be in the MeasureTheory namespace? If yes, then it's definitely unambiguous. OTOH, docs#MeasurableSpace is in the root NS.

[Felix Weilacher]

I was thinking to put it in the MeasurableSpace namespace