Hopf problem: hurewicz · higher hurewicz 1 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.HigherHurewicz.CubicalBoundary.whiskerFacet_symmAt_zero_apply
{n : ℕ}
{X : Type u_1}
[TopologicalSpace X]
{x : X}
(p : ↑(GenLoop (Fin (n + 1)) X x))
(u : Fin (n + 1) → ↑unitInterval)
: