English
If f is continuous and surjective between Polish spaces X and Y, then pushing forward the measurable structure along f yields exactly the Borel σ-algebra on Y: MeasurableSpace.map f (borel X) = borel Y.
Русский
Если f непрерывно и сюръективно отображает полиски пространства X в Y, то перенос борелевой сигма-алгебры по f дает ровно борелеву сигма-алгебру на Y: map_f(borel X) = borel Y.
LaTeX
$$$\\mathrm{MeasurableSpace.map}\,f\\; (\\mathrm{borel}\\,X) = \\mathrm{borel}\\,Y$$$
Lean4
theorem map_eq_borel {X Y : Type*} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
[TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f)
(hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = borel Y :=
by
borelize Y
exact hf.measurable.map_measurableSpace_eq hsurj
