Hopf problem: uniformization · triangle uniformization gluing

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

theorem Mathoverflow1973.TriangleUniformizationGluing.contMDiff_symm_of_contMDiff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace ℂ M] [ChartedSpace ℂ N] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ M] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ N] (e : M ≃ₜ N) (he : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ ⇑e) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ ⇑e.symm