comp_mdifferentiableWithinAt — Mathlib

English

Let g be differentiable and f be MDifferentiableWithinAt on a set s. Then the composition g ∘ f is MDifferentiableWithinAt on the same set s at x.

Русский

Пусть g дифференцируема, а f — MD-дифференцируемо внутри множества s в точке x. Тогда композиция g ∘ f дифференцируема внутри множества на той же точке x.

LaTeX

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

Lean4

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

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