English
If f is C^n between charted spaces, then its tangent map t f is C^m; i.e., differentiability lifts to the tangent level.
Русский
Если отображение f гладкое, то его касательный отображение tangentMap также гладкое на уровне tangent.
LaTeX
$$$\forall f:\, M \to M',\ ContMDiff I I' n f,\; (hmn : m + 1 ≤ n) \Rightarrow ContMDiff I.tangent I'.tangent m (tangentMap I I' f)$$$
Lean4
/-- The derivative `D_yf(y)` is `C^m` at `x₀`, where the derivative is taken as a continuous
linear map. We have to assume that `f` is `C^n` at `x₀` for some `n ≥ m + 1`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This is a special case of `ContMDiffAt.mfderiv` where `f` does not contain any parameters and
`g = id`.
-/
theorem mfderiv_const {x₀ : M} {f : M → M'} (hf : ContMDiffAt I I' n f x₀) (hmn : m + 1 ≤ n) :
ContMDiffAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderiv I I' f) x₀) x₀ :=
haveI : ContMDiffAt (I.prod I) I' n (fun x : M × M => f x.2) (x₀, x₀) := ContMDiffAt.comp (x₀, x₀) hf contMDiffAt_snd
this.mfderiv (fun _ => f) id contMDiffAt_id hmn
