English
A variant of the chain rule for derivatives of composition: the derivative of λy. g(f(y)) at x equals the derivative of g at f(x) composed with the derivative of f at x.
Русский
Альтернативная формулировка цепного правила для композиции: производная функции λy. g(f(y)) в точке x равна производной g в точке f(x), композиционно с производной f в x.
LaTeX
$$$$ \operatorname{fderiv}_{\mathbb{K}}( \lambda y. g(f(y)) ) x = \big( \operatorname{fderiv}_{\mathbb{K}} g (f x) \big) \circ \operatorname{fderiv}_{\mathbb{K}} f x. $$$$
Lean4
/-- A variant for the derivative of a composition, written without `∘`. -/
theorem fderiv_comp' {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
fderiv 𝕜 (fun y ↦ g (f y)) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
fderiv_comp x hg hf
