no goals
X : Type u_1
Y : Type ?u.692142
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.692157
F : Set X
⊢ PathConnectedSpace X ↔ ∃ x, pathComponent x = univ
simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]