English
Let f: E → F and g: E → G be ContDiffWithinAt on s at x. Then the map x ↦ f(x).smulRight (g(x)) is ContDiffWithinAt on s at x.
Русский
Пусть f: E → F и g: E → G гладки внутри s в точке x. Тогда отображение x ↦ f(x).smulRight (g(x)) гладко внутри s в x.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ n\ f\ s\ x \\land \\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ n\ g\ s\ x \\Rightarrow \\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ n\,(\lambda x. (f(x)).smulRight (g(x)))\ s\ x$$$
Lean4
@[fun_prop]
theorem smulRight {f : E → StrongDual 𝕜 F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => (f x).smulRight (g x)) s x :=
(isBoundedBilinearMap_smulRight (E := F)).contDiff.comp₂_contDiffWithinAt hf hg
