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