clm_prodMap — Mathlib

English

If g and f are ContMDiffAt at a point x, then the map x ↦ (g x).prodMap (f x) is ContMDiffAt at x.

Русский

Если g и f гладкие в точке x, то отображение x ↦ g(x).prodMap(f(x)) гладко в точке x.

LaTeX

$$$\forall {x : M}, (hg : ContMDiffAt I 𝓘(𝕜, F_1 \toL[𝕜] F_3) n g x) \land (hf : ContMDiffAt I 𝓘(𝕜, F_2 \toL[𝕜] F_4) n f x) \Rightarrow ContMDiffAt I 𝓘(𝕜, F_1 \times F_2 \toL[𝕜] F_3 \times F_4) n (\lambda x: (g x).prodMap (f x)) x$$

Lean4

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

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