clm_comp — Mathlib

English

Global differentiability of the map x ↦ g(x)(f(x)) when g and f are differentiable everywhere.

Русский

Глобальная дифференцируемость отображения x ↦ g(x)(f(x)).

LaTeX

$$$$MDifferentiable I 𝓘(𝕜, F_2) (\lambda x. g(x)(f(x)))$$$$

Lean4

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

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