comp_mdifferentiableWithinAt — Mathlib

English

If g is differentiable at f(x), and f is MDifferentiableWithinAt, then g∘f is MDifferentiableWithinAt at x provided MapsTo f s t.

Русский

Если g дифференцируемо в точке f(x), а f дифференцируемо внутри s, и f изображает s в t, то g∘f дифференцируем внутри t в точке x.

LaTeX

$$$ hg : DifferentiableAt 𝕜 g (f x) \; \to\; hf : MDifferentiableWithinAt I 𝓘(𝕜, F) f s x \to\; h : MapsTo f s t \; \Rightarrow\; MDifferentiableWithinAt I 𝓘(𝕜, F') (g \circ f) s x $$$

Lean4

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

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