comp_mdifferentiable — Mathlib

English

Let g be differentiable and f be MDifferentiableWithinAt on s. Then g ∘ f is MDifferentiableWithinAt on s at x.

Русский

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

LaTeX

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

Lean4

theorem comp_mdifferentiable {g : F → F'} {f : M → F} (hg : Differentiable 𝕜 g) (hf : MDifferentiable I 𝓘(𝕜, F) f) :
    MDifferentiable I 𝓘(𝕜, F') (g ∘ f) := fun x => hg.differentiableAt.comp_mdifferentiableAt (hf x)

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