borelSpace_codomain — Mathlib

English

A measurable image of a set under a measurable map from a standard Borel space to a Polish space is analytic.

Русский

Измеримое изображение множества под измеримой картой из стандартного борелова пространства в полиш-пространство есть аналитическое.

LaTeX

$$$f: X \to Y$ measurable, $X$ StandardBorelSpace, $Y$ PolishSpace, $s$ MeasurableSet \;\Rightarrow \; \operatorname{AnalyticSet}(f'' s).$$$

Lean4

theorem borelSpace_codomain [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f) (hsurj : Surjective f) :
    BorelSpace Y :=
  ⟨(hf.map_measurableSpace_eq hsurj).symm.trans <| hf.map_measurableSpace_eq_borel hsurj⟩

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