English
If hg is ContDiffAt 𝕜 n g and hf1, hf2 are ContDiffWithinAt 𝕜 n f1 s x, ContDiffWithinAt 𝕜 n f2 s x, then their composition is ContDiffWithinAt 𝕜 n (fun x => g (f1 x, f2 x)) s x.
Русский
Если hg — ContDiffAt 𝕜 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{ContDiffAt}_{\mathbb{k}}\ n\ g\ (f_1(x), f_2(x)) \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
theorem comp₂_contDiffWithinAt {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F} {x : F} (hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
ContDiffWithinAt 𝕜 n (fun x => g (f₁ x, f₂ x)) s x :=
hg.contDiffAt.comp_contDiffWithinAt x (hf₁.prodMk hf₂)
