measurableEmbedding — Mathlib

English

An injective continuous map on a Polish space is a measurable embedding: it is measurable, injective, and its image is a measurable embedding.

Русский

Инъективное непрерывное отображение на полиш-пространстве является измеримым вложением: измеримо, инъективно и образ является измеримым вложением.

LaTeX

$$MeasurableEmbedding f$$

Lean4

/-- An injective continuous function on a Polish space is a measurable embedding. -/
theorem measurableEmbedding [BorelSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ]
    (f_cont : Continuous f) (f_inj : Injective f) : MeasurableEmbedding f :=
  { injective := f_inj
    measurable := f_cont.measurable
    measurableSet_image' := fun _u hu => hu.image_of_continuousOn_injOn f_cont.continuousOn f_inj.injOn }

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