Hopf problem: foundations · euclidean sphere #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.EuclideanSphere.homotopic_refl_of_not_surjective
{n : ℕ}
{v : ↑((fun (n : ℕ) => Metric.sphere 0 1) n)}
(γ : Path v v)
(h : ¬Function.Surjective ⇑γ)
: