comp — Mathlib

English

If g is MDifferentiableAt at f(x) and f is MDifferentiableAt at x, then g∘f is MDifferentiableAt at x with the derivative equal to the composition of derivatives.

Русский

Если g дифференцируема в f(x) и f дифференцируема в x, то g∘f дифференцируема в x и её производная есть композиция производных.

LaTeX

$$$hg:\\nMDifferentiableAt I' I'' g (f x) \\;\\; hf:\\nMDifferentiableAt I I' f x \\Rightarrow MDifferentiableAt I I'' (g \\circ f) x$$$

Lean4

theorem comp (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
    MDifferentiableAt I I'' (g ∘ f) x :=
  (hg.hasMFDerivAt.comp x hf.hasMFDerivAt).mdifferentiableAt

Похожие утверждения