comp_mdifferentiableAt — Mathlib

English

Let g be differentiable and f be MDifferentiableAt; then g ∘ f is MDifferentiableAt.

Русский

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

LaTeX

$$$\text{Differentiable } 𝕜\ g \land \text{MDifferentiableAt } I\ 𝓘(𝕜, F)\ f\ x \Rightarrow\ MDifferentiableAt I\ 𝓘(𝕜, F')\ (g \circ f)\ x$$$

Lean4

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

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