English
If hg is ContDiff 𝕜 n g and f1, f2, f3 are ContDiffOn 𝕜 n on s, then x ↦ g(f1 x, f2 x, f3 x) is ContDiffOn 𝕜 n on s.
Русский
Если g — ContDiff 𝕜 n, а f1, f2, f3 — ContDiffOn 𝕜 n на s, то x ↦ g(f1 x, f2 x, f3 x) — ContDiffOn 𝕜 n на 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\ f_3 s \Rightarrow \mathrm{ContDiffOn}_{\mathbb{k}}\ n\ (x \mapsto g(f_1 x, f_2 x, f_3 x)) s.$$$
Lean4
@[fun_prop]
theorem clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X} {x : X} (hg : ContDiffWithinAt 𝕜 n g s x)
(hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun x => (g x).comp (f x)) s x :=
(isBoundedBilinearMap_comp (E := E) (G := G)).contDiff.comp₂_contDiffWithinAt hg hf
