comp_mdifferentiableAt — Mathlib

English

Let g be differentiable at f(x) and let f be MDifferentiableAt with respect to the model I at x. Then the composition g ∘ f is MDifferentiableAt (with respect to the same model) at x into F'.

Русский

Пусть g дифференцируема в точке f(x) и пусть f является MD-дифференцируемым в точке x относительно модели I. Тогда композиция g ∘ f дифференцируема в x.

LaTeX

$$$\text{Differentiable } 𝕜\ g \ (f\ x) \quad\text{and}\quad \text{MDifferentiableAt } I\ 𝓘(𝕜, F)\ f\ x \implies\ MDifferentiableAt I\ 𝓘(𝕜, F')\ (g \circ f)\ x$$$

Lean4

theorem comp_mdifferentiableAt {g : F → F'} {f : M → F} {x : M} (hg : DifferentiableAt 𝕜 g (f x))
    (hf : MDifferentiableAt I 𝓘(𝕜, F) f x) : MDifferentiableAt I 𝓘(𝕜, F') (g ∘ f) x :=
  hg.comp_mdifferentiableWithinAt hf

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