English
If hg is ContDiff 𝕜 n g, and hf1, hf2 are ContDiffWithinAt 𝕜 n f1 s x and ContDiffWithinAt 𝕜 n f2 s x, then x ↦ g (f1 x, f2 x) is ContDiffWithinAt 𝕜 n on s.
Русский
Если hg — ContDiff 𝕜 n g, а hf1, hf2 — ContDiffWithinAt 𝕜 n f1 s x и ContDiffWithinAt 𝕜 n f2 s x, то x ↦ g(f1(x), f2(x)) — ContDiffWithinAt 𝕜 n на s.
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
theorem comp₂_contDiffOn {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F} (hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffOn 𝕜 n f₁ s) (hf₂ : ContDiffOn 𝕜 n f₂ s) : ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ x)) s :=
hg.comp_contDiffOn <| hf₁.prodMk hf₂
