Hopf problem: main theorem · core 3

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

theorem Mathoverflow1973.mathoverflow_1973 : ∃ (atlas : ChartedSpace (EuclideanSpace ℂ (Fin 3)) ↑(unitSphere 6)), IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin 3))) 1 ↑(unitSphere 6)