English
Let g: F → G be differentiable at f(x) and f: E → F differentiable at x. Then the derivative of the composition g ∘ f at x is the composition of derivatives: fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)) ∘ (fderiv 𝕜 f x).
Русский
Пусть g: F→G дифференцируема в точке f(x) и f: E→F дифференцируема в x. Тогда производная композиции g ∘ f в x равна композиции производных: fderiv 𝕜 (g ∘ f) x = fderiv 𝕜 g (f x) ∘ fderiv 𝕜 f x.
LaTeX
$$$$ \operatorname{fderiv}_{\mathbb{K}}(g \circ f)\, x = \big( \operatorname{fderiv}_{\mathbb{K}} g (f x) \big) \circ \operatorname{fderiv}_{\mathbb{K}} f x. $$$$
Lean4
theorem fderiv_comp {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
(hg.hasFDerivAt.comp x hf.hasFDerivAt).fderiv
