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