X : Type u_1
Y : Type ?u.708006
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.708021
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
X : Type u_1
Y : Type ?u.708006
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.708021
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ IsPathConnected U ↔ IsConnected U
rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]
X : Type u_1
Y : Type ?u.708006
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.708021
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
this : LocPathConnectedSpace ↑U
⊢ PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
X : Type u_1
Y : Type ?u.708006
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.708021
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
⊢ PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
haveI := locPathConnected_of_isOpen U_op
no goals
X : Type u_1
Y : Type ?u.708006
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.708021
F : Set X
inst✝ : LocPathConnectedSpace X
U : Set X
U_op : IsOpen U
this : LocPathConnectedSpace ↑U
⊢ PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
exact pathConnectedSpace_iff_connectedSpace