comp_mdifferentiableWithinAt — Mathlib

English

The mfderiv equals the fderiv for maps between vector spaces.

Русский

mfderiv равен fderiv для отображений между векторными пространствами.

LaTeX

$$$ mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x $$$

Lean4

theorem comp_mdifferentiableWithinAt {g : F → F'} {f : M → F} {s : Set M} {t : Set F} {x : M}
    (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : MDifferentiableWithinAt I 𝓘(𝕜, F) f s x) (h : MapsTo f s t) :
    MDifferentiableWithinAt I 𝓘(𝕜, F') (g ∘ f) s x :=
  hg.mdifferentiableWithinAt.comp x hf h

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