case intro.intro.intro.intro
α : Type ?u.321538
inst✝⁵ : TopologicalSpace α
ι : Type ?u.321544
γ : Type u_1
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_2
tβ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
f : γ → β
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed s
right✝ : IsOpen s
⊢ MeasurableSet (f '' s)
α : Type ?u.321538
inst✝⁵ : TopologicalSpace α
ι : Type ?u.321544
γ : Type u_1
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_2
tβ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
f : γ → β
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
  ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
  hs.isClopenable
no goals
case intro.intro.intro.intro
α : Type ?u.321538
inst✝⁵ : TopologicalSpace α
ι : Type ?u.321544
γ : Type u_1
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_2
tβ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
f : γ → β
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
s_closed : IsClosed s
right✝ : IsOpen s
⊢ MeasurableSet (f '' s)
exact
  @IsClosed.measurableSet_image_of_continuousOn_injOn γ t' t'_polish β _ _ _ _ s s_closed f
    (f_cont.mono_dom t't) f_inj