map_borel_eq — Mathlib

English

If f is a continuous surjective map between Polish spaces X and Y, then the pushforward of the standard Borel on X is the Borel on Y: MeasurableSpace.map f (borel X) = borel Y.

Русский

Если f — непрерывное суръективное отображение между полскими пространствами X и Y, то образ борелевой сигма-алгебры по f равен борелевой сигма-алгебре на Y.

LaTeX

$$$\\mathrm{MeasurableSpace.map}\,f\\, (\\mathrm{borel}\\,X) = \\mathrm{borel}\\,Y$$$

Lean4

theorem map_borel_eq {X Y : Type*} [TopologicalSpace X] [PolishSpace X] [TopologicalSpace Y] [T0Space Y]
    [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f) (hsurj : Surjective f) :
    MeasurableSpace.map f (borel X) = borel Y := by
  borelize X
  exact hf.map_eq_borel hsurj

Похожие утверждения