prodMk_space — Mathlib

English

If f and g are ContMDiffOn on a set s, then the map x ↦ (f x, g x) is ContMDiffOn with product structure.

Русский

Если f и g гладкие на множестве s, то пара (f,g) гладкая на s в произведении пространств.

LaTeX

$$ContMDiffOn I I' n f s → ContMDiffOn I J' n g s → ContMDiffOn I (I'.prod J') n (λ x, { fst := f x, snd := g x }) s$$

Lean4

nonrec theorem prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiffAt I 𝓘(𝕜, E') n f x)
    (hg : ContMDiffAt I 𝓘(𝕜, F') n g x) : ContMDiffAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) x :=
  hf.prodMk_space hg

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