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