English
In a vector space, the scalar multiplication map is ContMDiff: the map (f, g) ↦ f · g is ContMDiff when f and g are ContMDiff.
Русский
Векторное пространство: отображение умножения на скаляр гладко зависимо: (f,g) ↦ f·g гладко, если f, g гладкие.
LaTeX
$$$\forall {f: M \to 𝕜} {g: M \to V},\ ContMDiff At I 𝓘(𝕜) n f x \land ContMDiffAt I 𝓘(𝕜, V) n g x \Rightarrow ContMDiffAt I 𝓘(𝕜, V) n (\lambda p: M, f p \cdot g p) x$$$
Lean4
theorem smul {f : M → 𝕜} {g : M → V} (hf : ContMDiffWithinAt I 𝓘(𝕜) n f s x)
(hg : ContMDiffWithinAt I 𝓘(𝕜, V) n g s x) : ContMDiffWithinAt I 𝓘(𝕜, V) n (fun p => f p • g p) s x :=
(contMDiff_smul.of_le le_top).contMDiffAt.comp_contMDiffWithinAt x (hf.prodMk hg)