English
If a measurable space on α is countably generated and separates points, there exists a second countable T4 topology on α whose Borel space is defined.
Русский
Если на α задано считываемое пространство, которое считываемо по счёту и разделяет точки, существует топология на α, которая является вторым счётом и T4, чья пространство Бореля задаёт эту структуру.
LaTeX
$$$\\exists \\tau : TopologicalSpace \\alpha,\\; SecondCountableTopology \\alpha \\wedge T4Space \\alpha \\wedge BorelSpace \\alpha$$$
Lean4
/-- 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). -/
theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type*) [m : MeasurableSpace α]
[CountablyGenerated α] [SeparatesPoints α] :
∃ _ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α :=
by
rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩
letI := induced f inferInstance
let F := f.toEquiv.toHomeomorphOfIsInducing <| .induced _
exact ⟨inferInstance, F.secondCountableTopology, F.symm.t4Space, f.measurableEmbedding.borelSpace F.isInducing⟩
