map_measurableSpace_eq_borel — Mathlib

English

If f: X → Y is measurable and surjective, then the measurable structure on Y equals the pushforward of X's measurable structure under f.

Русский

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

LaTeX

$$$\text{map } f\;\bigl(\text{MeasurableSpace } X\bigr) = \text{MeasurableSpace } Y$ (under the given hypotheses).$$

Lean4

theorem map_measurableSpace_eq_borel [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f)
    (hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = borel Y :=
  by
  have d := hf.mono le_rfl OpensMeasurableSpace.borel_le
  letI := borel Y; haveI : BorelSpace Y := ⟨rfl⟩
  exact d.map_measurableSpace_eq hsurj

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