measurableSet_image_of_continuousOn_injOn

English

If s ⊂ γ is closed, f is continuous on s and injective on s, then f''s is a measurable set.

Русский

Если s замкнуто в γ, функция f непрерывна на s и инъективна на s, то образ f''s измерим.

LaTeX

$$MeasurableSet (f '' s)$$

Lean4

theorem measurableSet_image_of_continuousOn_injOn [TopologicalSpace γ] [PolishSpace γ] {β : Type*} [TopologicalSpace β]
    [T2Space β] [MeasurableSpace β] [OpensMeasurableSpace β] {s : Set γ} (hs : IsClosed s) {f : γ → β}
    (f_cont : ContinuousOn f s) (f_inj : InjOn f s) : MeasurableSet (f '' s) :=
  by
  rw [image_eq_range]
  haveI : PolishSpace s := IsClosed.polishSpace hs
  apply measurableSet_range_of_continuous_injective
  · rwa [continuousOn_iff_continuous_restrict] at f_cont
  · rwa [injOn_iff_injective] at f_inj

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