English
If hf is ContDiff 𝕜 n of uncurry f, hg, hk are ContDiff 𝕜 n, and hnm holds, then x ↦ fderiv 𝕜 (f x) (g x) (k x) is ContDiff 𝕜 n.
Русский
Если hf — ContDiff 𝕜 n (uncurry f), hg, hk — ContDiff 𝕜 n, и hnm выполняется, то x ↦ fderiv 𝕜 (f x) (g x) (k x) непрерывно различна по n.
LaTeX
$$$ContDiff\ 𝕜\ n\ (Function.uncurry\ f)\; \to\; ContDiff\ 𝕜\ n\ g\; \to\ ContDiff\ 𝕜\ n\ k \to\ WithTop.preorder.le\ (n+1)\ m \to\ ContDiff\ 𝕜\ n\ (\lambda x. fderiv\ 𝕜\ (f x) (g x) (k x))$$$
Lean4
/-- `x ↦ fderiv 𝕜 (f x) (g x) (k x)` is smooth. -/
theorem fderiv_apply {f : E → F → G} {g k : E → F} (hf : ContDiff 𝕜 m <| Function.uncurry f) (hg : ContDiff 𝕜 n g)
(hk : ContDiff 𝕜 n k) (hnm : n + 1 ≤ m) : ContDiff 𝕜 n fun x => fderiv 𝕜 (f x) (g x) (k x) :=
(hf.fderiv hg hnm).clm_apply hk
