English
If hg is ContDiff 𝕜 n g and f1, f2, f3 are ContDiffOn 𝕜 n on s, then x ↦ g(f1 x, f2 x, f3 x) is ContDiffOn 𝕜 n on s.
Русский
Если g: E1 × E2 × E3 → G гладко порядка n на s и f1, f2, f3 — ContDiffOn 𝕜 n на s, то x ↦ g(f1 x, f2 x, f3 x) гладко порядка n на s.
LaTeX
$$$\mathrm{ContDiff}_{\mathbb{k}}\ n\ g\Rightarrow \mathrm{ContDiffOn}_{\mathbb{k}}\ n\ f_1 s \Rightarrow \mathrm{ContDiffOn}_{\mathbb{k}}\ n\ f_2 s \Rightarrow \mathrm{ContDiffOn}_{\mathbb{k}}\ n\ f_3 s \Rightarrow \mathrm{ContDiffOn}_{\mathbb{k}}\ n\ (x \mapsto g(f_1 x, f_2 x, f_3 x)) s.$$$
Lean4
theorem comp₃_contDiffOn {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃} {s : Set F}
(hg : ContDiff 𝕜 n g) (hf₁ : ContDiffOn 𝕜 n f₁ s) (hf₂ : ContDiffOn 𝕜 n f₂ s) (hf₃ : ContDiffOn 𝕜 n f₃ s) :
ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ x, f₃ x)) s :=
hg.comp₂_contDiffOn hf₁ <| hf₂.prodMk hf₃
