Commit 2024-09-03 16:29 e1258e0d

View on Github →

feat(MeasurableSpace): SeparatesPoints -> MeasurableSingletonClass (#16288)

  • If a σ-algebra on a countable type separates points, then singletons are measurable.
  • Generalize a lemma from T1Space to T0Space.

Estimated changes

modified theorem borel_eq_top_of_countable