scomp — Mathlib

English

If f is differentiable and g is differentiable, then (g ∘ f)' at x equals f'(x) times g'(f(x)).

Русский

Если f дифференцируема, и g дифференцируема, то (g ∘ f)' в x равна f'(x) · g'(f(x)).

LaTeX

$$$\text{If } f \text{ is differentiable at } x \text{ and } g \text{ is differentiable at } f(x), \text{ then } (g \circ f)'(x) = f'(x) \cdot g'(f(x)).$$$

Lean4

theorem scomp (hg : DifferentiableAt 𝕜' g₁ (h x)) (hh : DifferentiableAt 𝕜 h x) :
    deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x) :=
  (HasDerivAt.scomp x hg.hasDerivAt hh.hasDerivAt).deriv

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