mathlib

38341f11 - feat(algebraic_topology/fundamental_groupoid): Define simply connected spaces (#12788)

feat(algebraic_topology/fundamental_groupoid): Define simply connected spaces (#12788) Proves contractible spaces are simply connected, and that simply connected spaces are characterized by the property that any two paths between the same endpoints are homotopic.