clm_apply — Mathlib

English

If g: M → F1 →L F3 and f: M → F2 →L F4 are differentiable, then the map x ↦ (g x).prodMap (f x) is differentiable into F1 × F2 →L F3 × F4.

Русский

Если g и f дифференцируемы, то x ↦ (g x).prodMap (f x) дифференцируемо в пространство F1 × F2 →L F3 × F4.

LaTeX

$$$$MDifferentiableWithinAt I 𝓘(𝕜, F_1 \to_L F_3) g s x \land MDifferentiableWithinAt I 𝓘(𝕜, F_2 \to_L F_4) f s x \Rightarrow MDifferentiableWithinAt I 𝓘(𝕜, F_1 \times F_2 \to_L F_3 \times F_4) (\lambda x. (g x).prodMap (f x)) s x.$$$$

Lean4

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

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