clm_prodMap — Mathlib

English

At a point x, if g and f are differentiable, then x ↦ g(x) ∘ f(x) is differentiable at x.

Русский

В точке x композиция g(x) ∘ f(x) дифференцируема.

LaTeX

$$$$MDifferentiableAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) (\lambda x. g x \circ f x) x.$$$$

Lean4

nonrec theorem clm_prodMap {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₁ × F₂ →L[𝕜] F₃ × F₄) (fun x => (g x).prodMap (f x)) x :=
  Differentiable.comp_mdifferentiableWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2) (f :=
    fun x => (g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).differentiable (hg.prodMk_space hf)

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