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.
Русский
Если g — ContDiff 𝕜 n, а f1, f2 — ContDiffOn 𝕜 n на s, то x ↦ g(f1 x, f2 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\ (x \mapsto g(f_1 x, f_2 x)) s.$$$
Lean4
@[fun_prop]
theorem clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X} (hg : ContDiffOn 𝕜 n g s)
(hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun x => (g x).comp (f x)) s :=
(isBoundedBilinearMap_comp (E := E) (F := F) (G := G)).contDiff.comp₂_contDiffOn hg hf
