English
If hf : ContDiffOn 𝕜 n f s and hg : ContDiffOn 𝕜 n g s, then ContDiff 𝕜 n (x ↦ (f x, g x)) on s.
Русский
Если hf : ContDiffOn 𝕜 n f s и hg : ContDiffOn 𝕜 n g s, тогда ContDiff 𝕜 n (x ↦ (f(x), g(x))) на s.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f\,s \land \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,s \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} (x \mapsto (f(x), g(x)))\,s$$$
Lean4
/-- The Cartesian product of `C^n` functions at a point is `C^n`. -/
@[fun_prop]
theorem prodMk {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
ContDiffAt 𝕜 n (fun x : E => (f x, g x)) x :=
contDiffWithinAt_univ.1 <| hf.contDiffWithinAt.prodMk hg.contDiffWithinAt
