prodMk — Mathlib

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)

Похожие утверждения