case intro.intro.intro
α : Type ?u.322100
inst✝⁶ : TopologicalSpace α
ι : Type ?u.322106
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁵ : PolishSpace γ
inst✝⁴ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_1
tβ : TopologicalSpace β
inst✝³ : T2Space β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
s : Set γ
f : γ → β
inst✝ : SecondCountableTopology β
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
⊢ MeasurableSet (f '' s)
α : Type ?u.322100
inst✝⁶ : TopologicalSpace α
ι : Type ?u.322106
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁵ : PolishSpace γ
inst✝⁴ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_1
tβ : TopologicalSpace β
inst✝³ : T2Space β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
s : Set γ
f : γ → β
inst✝ : SecondCountableTopology β
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)
obtain ⟨t', t't, f_cont, t'_polish⟩ :
  ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ β t' tβ f ∧ @PolishSpace γ t' :=
  f_meas.exists_continuous
case intro.intro.intro
α : Type ?u.322100
inst✝⁶ : TopologicalSpace α
ι : Type ?u.322106
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁵ : PolishSpace γ
inst✝⁴ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_1
tβ : TopologicalSpace β
inst✝³ : T2Space β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
s : Set γ
f : γ → β
inst✝ : SecondCountableTopology β
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
M : MeasurableSet s
⊢ MeasurableSet (f '' s)
case intro.intro.intro
α : Type ?u.322100
inst✝⁶ : TopologicalSpace α
ι : Type ?u.322106
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁵ : PolishSpace γ
inst✝⁴ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_1
tβ : TopologicalSpace β
inst✝³ : T2Space β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
s : Set γ
f : γ → β
inst✝ : SecondCountableTopology β
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
⊢ MeasurableSet (f '' s)
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
no goals
case intro.intro.intro
α : Type ?u.322100
inst✝⁶ : TopologicalSpace α
ι : Type ?u.322106
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁵ : PolishSpace γ
inst✝⁴ : MeasurableSpace γ
hγb : BorelSpace γ
β : Type u_1
tβ : TopologicalSpace β
inst✝³ : T2Space β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
s : Set γ
f : γ → β
inst✝ : SecondCountableTopology β
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous f
t'_polish : PolishSpace γ
M : MeasurableSet s
⊢ MeasurableSet (f '' s)
exact
  @MeasurableSet.image_of_continuousOn_injOn γ t' t'_polish (@borel γ t')
    (@BorelSpace.mk _ _ (borel γ) rfl)
    β _ _ _ _ s f M (@Continuous.continuousOn γ β t' tβ f s f_cont) f_inj