α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type ?u.62127
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet s
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type ?u.62127
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
⊢ AnalyticSet s
haveI : PolishSpace s := hs.polishSpace
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type ?u.62127
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet (range Subtype.val)
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type ?u.62127
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet s
rw [← @Subtype.range_val α s]
no goals
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type ?u.62127
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet (range Subtype.val)
exact analyticSet_range_of_polishSpace continuous_subtype_val