English
If hf : ContDiffOn 𝕜 n f s and hg : ContDiffOn 𝕜 n g s, then ContDiffOn 𝕜 n (x ↦ (f x, g x)) s.
Русский
Если hf : ContDiffOn 𝕜 n f s и hg : ContDiffOn 𝕜 n g s, то ContDiffOn 𝕜 n (x ↦ (f x, g x)) s.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f\,s \to \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,s \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (x \mapsto (f(x),g(x)))\,s$$$
Lean4
/-- The Cartesian product of `C^n` functions on domains is `C^n`. -/
@[fun_prop]
theorem prodMk {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
ContDiffOn 𝕜 n (fun x : E => (f x, g x)) s := fun x hx => (hf x hx).prodMk (hg x hx)