instance PiBase.instSimplyConnectedSpaceOfPresimplyConnectedSpaceOfNonempty (X : Type u_1) [TopologicalSpace X] [h : PresimplyConnectedSpace X] [h' : Nonempty X] : SimplyConnectedSpace X

A nonempty, pre simply connected space is connected.

theorem PiBase.SimplyConnectedSpace.presimplyConnectedSpace (X : Type u_1) [TopologicalSpace X] [h : SimplyConnectedSpace X] : PresimplyConnectedSpace X

A simply connected space is pre simply connected.

theorem PiBase.WellDefined.presimplyConnectedSpace : WellDefined PresimplyConnectedSpace