English
If f: E → StrongDual 𝕜 F and g: E → G are ContDiff 𝕜 n, then x ↦ (f x).smulRight (g x) is ContDiff 𝕜 n.
Русский
Если f: E → StrongDual 𝕜 F и g: E → G гладкие порядка n, то x ↦ (f x).smulRight (g x) гладко порядка n.
LaTeX
$$$\mathrm{ContDiff}_{\mathbb{k}}\ n\ f \Rightarrow \mathrm{ContDiff}_{\mathbb{k}}\ n\ g \Rightarrow \mathrm{ContDiff}_{\mathbb{k}}\ n\ (x \mapsto \mathrm{f}(x) \smulRight \mathrm{g}(x)).$$$
Lean4
@[fun_prop]
theorem clm_apply {f : E → F →L[𝕜] G} {g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
ContDiffAt 𝕜 n (fun x => (f x) (g x)) x :=
isBoundedBilinearMap_apply.contDiff.comp₂_contDiffAt hf hg