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