instance PiBase.instPathConnectedSpaceOfPrepathConnectedSpaceOfNonempty (X : Type u_1) [TopologicalSpace X] [h : PrepathConnectedSpace X] [h' : Nonempty X] : PathConnectedSpace X

A nonempty, prepathconnected space is connected.

theorem PiBase.PathconnectedSpace.PrepathConnectedSpace (X : Type u_1) [TopologicalSpace X] [h : PathConnectedSpace X] : PiBase.PrepathConnectedSpace X

A pathconnectespace is prepathconnected.

theorem PiBase.WellDefined.prepathConnectedSpace : WellDefined PrepathConnectedSpace

theorem PiBase.Homeomorph.prepathConnectedSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : PrepathConnectedSpace X] (f : X ≃ₜ Y) : PrepathConnectedSpace Y