Hopf problem: threefold · six sphere complex atlas

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

theorem Mathoverflow1973.SixSphereComplexAtlas.exists_complex_analytic_atlas : ∃ (atlas : ChartedSpace (EuclideanSpace ℂ (Fin 3)) ↑(unitSphere 6)), IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin 3))) ⊤ ↑(unitSphere 6)

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