smul — Mathlib

English

Scalar multiplication on a product space is smooth: (f,g) ↦ f·g is ContMDiff.

Русский

Умножение на скаляр в произведении векторных пространств гладко: (f,g) ↦ f·g.

LaTeX

$$$\forall {f : M \to 𝕜} {g : M \to V},\ ContMDiffAt (modelWithCornersSelf 𝕜 𝕜) n f x \rightarrow ContMDiffAt (modelWithCornersSelf 𝕜 V) n g x \rightarrow ContMDiffAt (modelWithCornersSelf 𝕜 V) n (fun p => f p • g p) x$$$

Lean4

theorem smul {f : M → 𝕜} {g : M → V} (hf : ContMDiff I 𝓘(𝕜) n f) (hg : ContMDiff I 𝓘(𝕜, V) n g) :
    ContMDiff I 𝓘(𝕜, V) n fun p => f p • g p := fun x => (hf x).smul (hg x)

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