Commit 2022-05-03 14:29 6d2788c2

feat(analysis/calculus/cont_diff): cont_diff_succ_iff_fderiv_apply (#13797)

• Prove that a map is C^(n+1) iff it is differentiable and all its directional derivatives in all points are C^n.
• Also some supporting lemmas about continuous_linear_equiv.
• We only manage to prove this when the domain is finite dimensional.
• Prove one direction of cont_diff_on_succ_iff_fderiv_within with fewer assumptions
• From the sphere eversion project Co-authored by: Patrick Massot patrick.massot@u-psud.fr Co-authored by: Oliver Nash github@olivernash.org