Higher differentiability in finite dimensions. #
Finite dimensional results #
A family of continuous linear maps is C^n
on s
if all its applications are.
This is a useful lemma to prove that a certain operation preserves functions being C^n
.
When you do induction on n
, this gives a useful characterization of a function being C^(n+1)
,
assuming you have already computed the derivative. The advantage of this version over
contDiff_succ_iff_fderiv
is that both occurrences of ContDiff
are for functions with the same
domain and codomain (E
and F
). This is not the case for contDiff_succ_iff_fderiv
, which
often requires an inconvenient need to generalize F
, which results in universe issues
(see the discussion in the section of ContDiff.comp
).
This lemma avoids these universe issues, but only applies for finite dimensional E
.