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 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.

Estimated changes