prodMk — Mathlib

English

If hf : ContDiff 𝕜 n f and hg : ContDiff 𝕜 n g, then the map x ↦ (f x, g x) is ContDiff 𝕜 n.

Русский

Если f и g — C^n, то отображение x ↦ (f x, g x) — C^n.

LaTeX

$$$ \operatorname{ContDiff}_{\mathbb{K}}^{n} f \;\land\; \operatorname{ContDiff}_{\mathbb{K}}^{n} g \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} (x \mapsto (f(x),g(x)))$$$

Lean4

/-- The Cartesian product of `C^n` functions is `C^n`. -/
@[fun_prop]
theorem prodMk {f : E → F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x : E => (f x, g x) :=
  contDiffOn_univ.1 <| hf.contDiffOn.prodMk hg.contDiffOn

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