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