Typeclass abbreviating another.

Stream: mathlib4

[Felix Weilacher]

I would like to add a Typeclass abbreviating for HasCountableSeparatingOn _ MeasurableSet univ as in the code below.

class CountablySeparated (α : Type*) [MeasurableSpace α] : Prop where
  countably_separated : HasCountableSeparatingOn α MeasurableSet univ

instance [MeasurableSpace α] [h : HasCountableSeparatingOn α MeasurableSet univ] :
    CountablySeparated α := ⟨h⟩

instance [MeasurableSpace α] [h : CountablySeparated α] :
    HasCountableSeparatingOn α MeasurableSet univ := h.countably_separated

Is this the most efficient way to accomplish what is basically just notation? In particular I am worried that the instance loop might be unoptimal somehow.

[Sébastien Gouëzel]

Is that equivalent to [CountablyGenerated α] [MeasurableSingletonClass α]?

[Felix Weilacher]

It is equivalent to the existence of a coarser sigma algebra with those properties

[Felix Weilacher]

see docs#MeasurableSpace.exists_countablyGenerated_le_of_hasCountableSeparatingOn

[Felix Weilacher]

and docs#MeasurableSpace.measurableSingletonClass_of_hasCountableSeparatingOn

[Sébastien Gouëzel]

Thanks for the clarification! (For instance, Lebesgue measurable sets are countably separated but not countably generated). Introducing a typeclass like you want to do is perfectly reasonable, and there is no issue with instance loops.

[Felix Weilacher]

ok, thanks!