α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (range fun x => f ↑x)
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)
rw [image_eq_range]
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ MeasurableSet (range fun x => f ↑x)
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (range fun x => f ↑x)
haveI : PolishSpace s := IsClosed.polishSpace hs
case f_cont
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Continuous fun x => f ↑x

case f_inj
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Injective fun x => f ↑x
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ MeasurableSet (range fun x => f ↑x)
apply measurableSet_range_of_continuous_injective
no goals
case f_cont
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Continuous fun x => f ↑x
rwa [continuousOn_iff_continuous_restrict] at f_cont
no goals
case f_inj
α : Type ?u.320629
inst✝⁵ : TopologicalSpace α
ι : Type ?u.320635
γ : Type u_2
tγ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_1
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set γ
hs : IsClosed s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Injective fun x => f ↑x
rwa [injOn_iff_injective] at f_inj