Hopf problem: hurewicz · sixth hurewicz

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

theorem Mathoverflow1973.SixthHurewicz.toLoop_transAt {X : Type} [TopologicalSpace X] {x : X} (p q : ↑(GenLoop (Fin 6) X x)) : GenLoop.toLoop 0 (GenLoop.transAt 0 p q) = Path.trans (GenLoop.toLoop 0 p) (GenLoop.toLoop 0 q)