Hopf problem: threefold · special periods 7

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

theorem Mathoverflow1973.SpecialPeriods.EllipticFilling.localDiffeomorphAt_of_comp {E : Type u_1} {F : Type u_2} {K : Type u_3} {M : Type u_4} {N : Type u_5} {T : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup K] [NormedSpace ℂ K] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [TopologicalSpace T] [ChartedSpace K T] {q : M → N} {f : N → T} {x : M} (hq : IsLocalDiffeomorphAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ F) ⊤ q x) (hf : IsLocalDiffeomorphAt (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ K) ⊤ (f ∘ q) x) : IsLocalDiffeomorphAt (modelWithCornersSelf ℂ F) (modelWithCornersSelf ℂ K) ⊤ f (q x)