Connectedness of Euclidean spheres

The unit sphere in EuclideanSpace ℝ (Fin m) is connected for m ≥ 2. TauCeti.connectedSpace_euclideanSphere supplies the connected-space instance used by covering-space and separation arguments on spheres, independently of their manifold structure.

theorem TauCeti.connectedSpace_euclideanSphere {m : ℕ} (hm : 1 < m) : ConnectedSpace ↑(Metric.sphere 0 1)

The unit sphere of ℝᵐ is connected for m ≥ 2.