English
If s is Borel, f is continuous on s and injective on s, then the restricted map s → f(s) is a measurable embedding.
Русский
Если s борелево и f непрерывна и инъективна на s, то ограниченное отображение s → f(s) является измеримым вложением.
LaTeX
$$MeasurableEmbedding (s.restrict f)$$
Lean4
/-- If `s` is Borel-measurable in a Polish space and `f` is continuous injective on `s`, then
the restriction of `f` to `s` is a measurable embedding. -/
theorem measurableEmbedding [BorelSpace β] [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ]
(hs : MeasurableSet s) (f_cont : ContinuousOn f s) (f_inj : InjOn f s) : MeasurableEmbedding (s.restrict f) :=
{ injective := injOn_iff_injective.1 f_inj
measurable := (continuousOn_iff_continuous_restrict.1 f_cont).measurable
measurableSet_image' := by
intro u hu
have A : MeasurableSet (((↑) : s → γ) '' u) := (MeasurableEmbedding.subtype_coe hs).measurableSet_image.2 hu
have B : MeasurableSet (f '' (((↑) : s → γ) '' u)) :=
A.image_of_continuousOn_injOn (f_cont.mono (Subtype.coe_image_subset s u))
(f_inj.mono (Subtype.coe_image_subset s u))
rwa [← image_comp] at B }
