Simply connected spaces #
This file defines simply connected spaces.
A topological space is simply connected if its fundamental groupoid is equivalent to Unit
.
Main theorems #
-
simply_connected_iff_unique_homotopic
- A space is simply connected if and only if it is nonempty and there is a unique path up to homotopy between any two points -
SimplyConnectedSpace.ofContractible
- A contractible space is simply connected
- equiv_unit : Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
A simply connected space is one whose fundamental groupoid is equivalent to Discrete Unit
Instances
In a simply connected space, any two paths are homotopic
A space is simply connected iff it is path connected, and there is at most one path up to homotopy between any two points.
Another version of simply_connected_iff_paths_homotopic