comp_hasFDerivAt_of_eq — Mathlib

English

If y = f(x) and hg: HasFDerivWithinAt g t y holds along with hf: HasFDerivAt f x', and hy: y = f(x), then HasFDerivAt for the composition g ∘ f at x holds.

Русский

Если y = f(x) и выполняются соответствующие условия внутри и вне, то производная композиции существует в x.

LaTeX

$$$\text{HasFDerivAt} (g\circ f) x = g'\circ f' x$ при hy$$

Lean4

theorem comp_hasFDerivAt_of_eq {g : F → G} {g' : F →L[𝕜] G} {t : Set F} {y : F} (hg : HasFDerivWithinAt g g' t y)
    (hf : HasFDerivAt f f' x) (ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) (hy : y = f x) : HasFDerivAt (g ∘ f) (g' ∘L f') x := by
  subst y; exact hg.comp_hasFDerivAt x hf ht

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