clm_comp — Mathlib

English

Within-At differentiability of the composition map x ↦ g(x) ∘ f(x) when g and f are differentiable within their respective spaces.

Русский

Дифференцируемость внутри множества композиции отображений g и f.

LaTeX

$$$$MDifferentiableWithinAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) (\lambda x. g x ∘ f x) s x.$$$$

Lean4

theorem clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} (hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) g x)
    (hf : MDifferentiableAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) f x) :
    MDifferentiableAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) (fun x => (g x).comp (f x)) x :=
  (hg.mdifferentiableWithinAt.clm_comp hf.mdifferentiableWithinAt).mdifferentiableAt Filter.univ_mem

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