clm_apply — Mathlib

English

Within a set s, if g and f are differentiable on s, then the composition x ↦ g(x)(f(x)) is differentiable on s.

Русский

На множестве s дифференцируемо отображение x ↦ g(x)(f(x)).

LaTeX

$$$$\text{If } hf: MDifferentiableOn I 𝓘(𝕜, F_1 \to_L[𝕜] F_2) f s \text{ and } hg: MDifferentiableOn I 𝓘(𝕜, F_1) g s, \\ MDifferentiableOn I 𝓘(𝕜, F_2) (\lambda x. g(x)(f(x))) s.$$$$

Lean4

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

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