measurableEmbedding — Mathlib

English

A measurable embedding exists for a measurable injective map from a standard Borel space to a countably separated measurable space.

Русский

Для измеримого инъективного отображения между стандартными пространствами Бореля существует измеримое вложение.

LaTeX

$$MeasurableEmbedding f$$

Lean4

/-- An injective measurable function from a standard Borel space to a
countably separated measurable space is a measurable embedding. -/
theorem measurableEmbedding {f : γ → α} [MeasurableSpace.CountablySeparated α] [MeasurableSpace γ]
    [StandardBorelSpace γ] (f_meas : Measurable f) (f_inj : Injective f) : MeasurableEmbedding f :=
  { injective := f_inj
    measurable := f_meas
    measurableSet_image' := fun _u hu => hu.image_of_measurable_injOn f_meas f_inj.injOn }

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