English
If α is countably separated, there exists a second countable T4 topology on α such that open sets are measurable.
Русский
Если α представимо разделимо по счётности, существует топология на α, являющаяся вторым счетом и T4, для которой открытые множества измеримы.
LaTeX
$$$\\exists \\tau : TopologicalSpace \\alpha,\\; SecondCountableTopology \\alpha \\wedge T4Space \\alpha \\wedge OpensMeasurableSpace \\alpha$$$
Lean4
/-- If a measurable space on `α` is countably generated and separates points, there is some
second countable t4 topology on `α` (i.e. a separable metrizable one) for which every
open set is measurable. -/
theorem exists_opensMeasurableSpace_of_countablySeparated (α : Type*) [m : MeasurableSpace α] [CountablySeparated α] :
∃ _ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α :=
by
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩
exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩
