English
If the curried map f: E → F → G is C^n in the sense of its uncurry, and g: E → F is continuous, then the map x ↦ fderiv 𝕜 (f x) (g x) is a continuous map from E into the space of linear maps E → G.
Русский
Если функция f: E → F → G имеет класc непрерывности C^n по цепочке (через несущую), и g: E → F непрерывна, то функция x ↦ fderiv 𝕜 (f x) (g x) непрерывна как отображение x в пространство линейных отображений E → G.
LaTeX
$$$ContDiff\ 𝕜\ n\ (Function.uncurry\ f)\; \to\; Continuous\ g\; \to\; 1 \le n\; \to\; \text{Continuous}\left( x \mapsto fderiv\ 𝕜\ (f\ x)\ (g\ x)\right)$$$
Lean4
/-- `x ↦ fderiv 𝕜 (f x) (g x)` is continuous. -/
theorem fderiv {f : E → F → G} {g : E → F} (hf : ContDiff 𝕜 n <| Function.uncurry f) (hg : Continuous g) (hn : 1 ≤ n) :
Continuous fun x => fderiv 𝕜 (f x) (g x) :=
(hf.fderiv (contDiff_zero.mpr hg) hn).continuous
