English
If g: E1 × E2 → G is ContDiffAt at f1(x), f2(x), and f1, f2 are ContDiffAt 𝕜 n at x, then x ↦ g(f1(x), f2(x)) is ContDiffAt 𝕜 n at x.
Русский
Если g — ContDiffAt в точке (f1(x), f2(x)) и f1, f2 — ContDiffAt в x, то x ↦ g(f1(x), f2(x)) — ContDiffAt в x.
LaTeX
$$$\mathrm{ContDiffAt}_{\mathbb{k}}\ n\ g (f_1(x), f_2(x)) \land \mathrm{ContDiffAt}_{\mathbb{k}}\ n\ f_1\ x \land \mathrm{ContDiffAt}_{\mathbb{k}}\ n\ f_2\ x \Rightarrow \mathrm{ContDiffAt}_{\mathbb{k}}\ n\ (x \mapsto g(f_1(x), f_2(x)))\ x.$$$
Lean4
theorem comp₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {x : F} (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x))
(hf₁ : ContDiffAt 𝕜 n f₁ x) (hf₂ : ContDiffAt 𝕜 n f₂ x) : ContDiffAt 𝕜 n (fun x => g (f₁ x, f₂ x)) x :=
hg.comp x (hf₁.prodMk hf₂)
