Hopf problem: cusp fibre · cusp specialization

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

theorem Mathoverflow1973.CuspSpecialization.sourceCoordinateProjection_isOpenQuotientMap : IsOpenQuotientMap ⇑(PeriodTorusHigherHomology.coordinateProjection 2)