Theorems · Theorem · measure theory

exists_borelSpace_of_countablyGenerated_of_separatesPoints

∀ (α : Type u_5) [m : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] [MeasurableSpace.SeparatesPoints α],
  ∃ x, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

If a measurable space is countably generated and separates points, it arises as the Borel sets of some second countable t4 topology (i.e. a separable metrizable one).

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace.CountablyGeneratedMeasurableSpace.SeparatesPoints