scomp_of_eq — Mathlib

English

If h₂ has derivative h₂' at f x and f has Frechet derivative f' at x, then (h₂ ∘ f) has Frechet derivative h₂' · f' at x.

Русский

Если h₂ имеет Фрéш-дериватив в f x, а f имеет Фрéш-дериватив в x, то (h₂ ∘ f) имеет дериватив h₂' · f' в x.

LaTeX

$$$\text{If } h_2 \text{ has derivative } h_2' \text{ at } f(x) \text{ and } f \text{ has Frechet derivative } f' \text{ at } x, \text{ then } h_2 \circ f \text{ has derivative } h_2' \cdot f' \text{ at } x.$$$

Lean4

theorem scomp_of_eq (hg : DifferentiableAt 𝕜' g₁ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) :
    deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x) := by rw [hy] at hg; exact deriv.scomp x hg hh

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