comp_hasDerivAt_of_eq — Mathlib

English

If hl is the Fréchet derivative of l at y with y = f(x), hf is a derivative of f at x, and hst maps, then the derivative of l ∘ f at x is given by l' f'.

Русский

Если hl — Фреше-дериватив L в y и y = f(x), hf — производная f в x, и отображение сохраняется, то дериватив композиции равен l' f'.

LaTeX

$$$$HasFDerivWithinAt l l' t y \land HasDerivWithinAt f f' s x \land MapsTo f s t \Rightarrow HasDerivWithinAt (l \circ f) (l' f') s x$$$$

Lean4

theorem comp_hasDerivAt_of_eq {t : Set F} (hl : HasFDerivWithinAt l l' t y) (hf : HasDerivAt f f' x)
    (ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) (hy : y = f x) : HasDerivAt (l ∘ f) (l' f') x := by subst y;
  exact hl.comp_hasDerivAt x hf ht

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