English
If t is measurable and g is monotone on t and continuous on t, then the image g''t is measurable.
Русский
Если t измеримо и g монотонна на t, непрерывна на t, то образ g(t) измерим.
LaTeX
$$MeasurableSet (g '' t)$$
Lean4
/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a standard Borel space,
then its image under a measurable injective map taking values in a
countably separate measurable space is also Borel-measurable. -/
theorem image_of_measurable_injOn {f : γ → α} [MeasurableSpace.CountablySeparated α] [MeasurableSpace γ]
[StandardBorelSpace γ] (hs : MeasurableSet s) (f_meas : Measurable f) (f_inj : InjOn f s) :
MeasurableSet (f '' s) := by
letI := upgradeStandardBorel γ
let tγ : TopologicalSpace γ := inferInstance
rcases exists_opensMeasurableSpace_of_countablySeparated α with
⟨τ, _, _, _⟩
-- for a finer Polish topology, `f` is continuous. Therefore, one may apply the corresponding
-- result for continuous maps.
obtain ⟨t', t't, f_cont, t'_polish⟩ :
∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' := f_meas.exists_continuous
have M : MeasurableSet[@borel γ t'] s :=
@Continuous.measurable γ γ t' (@borel γ t')
(@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)) tγ _ _ _
(continuous_id_of_le t't) s hs
exact
@MeasurableSet.image_of_continuousOn_injOn γ _ _ _ _ s f _ t' t'_polish (@borel γ t')
(@BorelSpace.mk _ _ (borel γ) rfl) M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj
