English
If s is measurable, f is measurable on γ, and f is injective on s, then the image f''s is measurable.
Русский
Если s измеримо, f измеримо на γ и инъективно на s, то образ f''s измерим.
LaTeX
$$MeasurableSet (f '' s)$$
Lean4
/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under
a continuous injective map is also Borel-measurable. -/
theorem image_of_continuousOn_injOn [OpensMeasurableSpace β] [tγ : TopologicalSpace γ] [PolishSpace γ]
[MeasurableSpace γ] [BorelSpace γ] (hs : MeasurableSet s) (f_cont : ContinuousOn f s) (f_inj : InjOn f s) :
MeasurableSet (f '' s) :=
by
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs.isClopenable
exact
@IsClosed.measurableSet_image_of_continuousOn_injOn γ t' t'_polish β _ _ _ _ s s_closed f (f_cont.mono_dom t't)
f_inj
