Hopf problem: homology theory · sphere homology 1

Supporting definitions and proofs for this stage of the six-sphere construction.

@[reducible, inline]

abbrev Mathoverflow1973.SphereHomology.UnitSphere (n : ℕ) : Set (EuclideanSpace ℝ (Fin (n + 1)))

The unit n-sphere in Euclidean (n+1)-space.

Equations

• Mathoverflow1973.SphereHomology.UnitSphere n = Metric.sphere 0 1