clm_prodMap — Mathlib

English

On a set, if g and f are differentiable on the set, then the composition is differentiable on the set.

Русский

На множестве композиция дифференцируема на этом множестве.

LaTeX

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

Lean4

theorem clm_prodMap {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : Set M}
    (hg : MDifferentiableOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) g s) (hf : MDifferentiableOn I 𝓘(𝕜, F₂ →L[𝕜] F₄) f s) :
    MDifferentiableOn I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) (fun x => (g x).prodMap (f x)) s := fun x hx =>
  (hg x hx).clm_prodMap (hf x hx)

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