English
If hf, hg, hk are C^n on a set s with unique differentiability, and m n satisfy m+1 ≤ n, then the map (x, y) ↦ (fderivWithin 𝕜 f s x) y is C^n on s × univ.
Русский
Если hf, hg, hk являются C^n на множество s с уникальностью дифференцируемости, и m+1 ≤ n, то отображение (x, y) ↦ fderivWithin 𝕜 f s x (y) на s × унив является C^n.
LaTeX
$$$ContDiffOn\ 𝕜\ n f\ s\; \to\; UniqueDiffOn\ 𝕜\ s\; \to\; m+1 \le n\; \to\; ContDiffOn\ 𝕜\ m\ (\lambda p: E\times E.\ (fderivWithin\ 𝕜\ f\ s\ p.1 : E \toL[𝕜] F)\ p.2)\ (s\ ×\ˢ\ univ)$$$
Lean4
@[fun_prop]
protected theorem fderiv_two {f : E → F → G} {g : E → F} (hf : ContDiff 𝕜 2 <| Function.uncurry f)
(hg : ContDiff 𝕜 1 g) : Differentiable 𝕜 fun x => fderiv 𝕜 (f x) (g x) :=
ContDiff.differentiable (contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt (le_refl 2))
(le_refl 1)
