Commit 2024-05-03 07:45 7e9dce6a

feat(MeasureTheory): add CountablySeparated (#12433) add a typeclass CountablySeparated _ abbreviating HasCountableSeparatingOn _ MeasurableSet univ. This is a common assumption is measure theory and is already used often in the library. Additionally, mathlib was previously not consistent in choosing between the equivalent spellings HasCountableSeparatingOn X MeasurableSet s and HasCountableSeparatingOn s MeasurableSet univ for X a measurable space and s : Set X. (In the latter spelling, s is being coerced to the subtype of X.) Lemmas and instances are added to help unify the situation. This is now spelled CountablySeparated s.