Commit 2024-03-25 19:10 ac9ad40f
View on Github →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 definesSeparatesPoints
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 SpaceNat -> Bool
. This will be used to generalize topological assumptions to measure theoretic ones in some theorems inMeasureTheory.Constructions.Polish
.