Basic properties of homotopy groups #
A pointed space is path connected if and only if its zeroth homotopy set is a subsingleton. This follows from Mathlib's equivalence between the zeroth homotopy set and path components.
theorem
TauCeti.pathConnectedSpace_iff_subsingleton_homotopyGroup_zero
{X : Type u_1}
[TopologicalSpace X]
(x : X)
:
A pointed space is path connected if and only if its zeroth homotopy set π_ 0 X x is a
subsingleton.