Commit 2024-03-25 19:10 ac9ad40f

feat(MeasureTheory.MeasurableSpace.CountablyGenerated): add SeparatesPoints and related theorems (#11048) the goal of the PR is to clarify the relationship between the following closely related assumptions on a measurable space:

• Being countably generated (CountablyGenerated)
• Separating points (SeparatesPoints)
• Having a countable separating family of measurable sets (HasCountableSeparatingOn _ MeasurableSet univ)
• Having singletons be measurable (MeasurableSingletonClass) It defines SeparatesPoints and registers all implications between combinations of these properties as instances (or rather a minimal set needed to deduce all others). It also proves an optimal theorem regarding when a measurable space appears as an induced subspace of the Cantor Space Nat -> Bool. This will be used to generalize topological assumptions to measure theoretic ones in some theorems in MeasureTheory.Constructions.Polish.