Hopf problem: foundations · canonical product

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

theorem Mathoverflow1973.CanonicalProduct.isLocalDiffeomorph_prodLine {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {f : M → N} (hf : IsLocalDiffeomorph (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) ⊤ f) : IsLocalDiffeomorph ((modelWithCornersSelf ℂ E).prod (modelWithCornersSelf ℂ ℂ)) ((modelWithCornersSelf ℂ F).prod (modelWithCornersSelf ℂ ℂ)) ⊤ fun (q : M × ℂ) => (f q.1, q.2)