X : Type u_1
Y : Type ?u.695184
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.695199
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace ↑F
X : Type u_1
Y : Type ?u.695184
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.695199
F : Set X
hF : IsPathConnected F
⊢ IsConnected F
rw [isConnected_iff_connectedSpace]
X : Type u_1
Y : Type ?u.695184
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.695199
F : Set X
hF : PathConnectedSpace ↑F
⊢ ConnectedSpace ↑F
X : Type u_1
Y : Type ?u.695184
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.695199
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace ↑F
rw [isPathConnected_iff_pathConnectedSpace] at hF
no goals
X : Type u_1
Y : Type ?u.695184
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.695199
F : Set X
hF : PathConnectedSpace ↑F
⊢ ConnectedSpace ↑F
exact @PathConnectedSpace.connectedSpace _ _ hF