English
The smul operation is smooth inside ContMDiffWithinAt: if f and g are ContMDiffWithinAt, then their scalar product is ContMDiffWithinAt.
Русский
Операция умножения на скаляр гладкая внутри ContMDiffWithinAt: если f,g гладкие внутри, то f·g гладко зависит от входа.
LaTeX
$$$\forall {f : M \to 𝕜} {g : M \to V},\ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 𝕜) n f s x \rightarrow ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n g s x \rightarrow ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n (fun p => f p \cdot g p) s x$$$
Lean4
nonrec theorem smul {f : M → 𝕜} {g : M → V} (hf : ContMDiffAt I 𝓘(𝕜) n f x) (hg : ContMDiffAt I 𝓘(𝕜, V) n g x) :
ContMDiffAt I 𝓘(𝕜, V) n (fun p => f p • g p) x :=
hf.smul hg
