English
The map x ↦ fderiv 𝕜 (f x) (g x) is contDiff at x₀ if f and g are contDiff at x₀ and appropriate conditions hold.
Русский
Отображение x ↦ fderiv 𝕜 (f x) (g x) гладко в точке x₀, если f и g гладкие в этой точке и выполняются условия.
LaTeX
$$$\operatorname{ContDiffAt}_{\mathbb{K}} n \ (fderiv\ 𝕜 (f x) (g x))\ x_0$$$
Lean4
/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth at `x₀`. -/
protected theorem fderiv {f : E → F → G} {g : E → F} (hf : ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀))
(hg : ContDiffAt 𝕜 m g x₀) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀ :=
by
simp_rw [← fderivWithin_univ]
refine
(ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ hmn (mem_univ x₀)
?_).contDiffAt
univ_mem
rw [preimage_univ]
