α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.1515
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range fun x => f ↑x)
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.1515
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (f '' s)
rw [image_eq_range]
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.1515
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
this : PolishSpace ↑s
⊢ AnalyticSet (range fun x => f ↑x)
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.1515
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range fun x => f ↑x)
haveI : PolishSpace s := hs.polishSpace
no goals
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type ?u.1515
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
this : PolishSpace ↑s
⊢ AnalyticSet (range fun x => f ↑x)
exact analyticSet_range_of_polishSpace (f_cont.comp continuous_subtype_val)