Hopf problem: recognition · smale 6

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

theorem Mathoverflow1973.Smale.StripCoordinates.hasDerivAt_verticalSlice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ℝ → E} {t s : ℝ} (hF : DifferentiableAt ℝ F (t, s)) : HasDerivAt (fun (u : ℝ) => F (t, u)) ((fderiv ℝ F (t, s)) (0, 1)) s