map_measurableSpace_eq — Mathlib

English

If f: X → Y is measurable and surjective with X a Polish space, then Y can be endowed with a Borel structure via the pushforward that matches the standard Borel structure on Y.

Русский

Если f: X → Y измеримо и сюръективно, и X полишпространство, то Y может получить борелеву структуру через образ, совпадающую со стандартной борелевой структурой на Y.

LaTeX

$$$\text{Measurable } f \land \text{Surjective } f \Rightarrow \text{BorelSpace } Y$ (constructed as in the statement).$$

Lean4

theorem map_measurableSpace_eq [CountablySeparated Z] {f : X → Z} (hf : Measurable f) (hsurj : Surjective f) :
    MeasurableSpace.map f ‹MeasurableSpace X› = ‹MeasurableSpace Z› :=
  MeasurableSpace.ext fun _ => hf.measurableSet_preimage_iff_of_surjective hsurj

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