English
If hg is ContDiffAt 𝕜 n g, and hf1, hf2 are ContDiffAt 𝕜 n f1 x, ContDiffAt 𝕜 n f2 x, then ContDiffAt 𝕜 n (λx. g(f1 x, f2 x)) x.
Русский
Если hg — ContDiffAt 𝕜 n g, а hf1, hf2 — ContDiffAt 𝕜 n f1 x и ContDiffAt 𝕜 n f2 x, то ContDiffAt 𝕜 n (λx. g(f1 x, f2 x)) x.
LaTeX
$$$\mathrm{ContDiffAt}_{\mathbb{k}}\ n\ g\ (f_1(x), 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₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃} (hg : ContDiff 𝕜 n g)
(hf₁ : ContDiff 𝕜 n f₁) (hf₂ : ContDiff 𝕜 n f₂) (hf₃ : ContDiff 𝕜 n f₃) :
ContDiff 𝕜 n fun x => g (f₁ x, f₂ x, f₃ x) :=
hg.comp₂ hf₁ <| hf₂.prodMk hf₃
