# Commit 2022-05-03 14:29 6d2788c2

View on Github →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