prodMk_space — Mathlib

English

If f : M → E' and g : M → F' are C^n in the appropriate model spaces, then the pair map x ↦ (f(x), g(x)) is C^n into E' × F'.

Русский

Если f : M → E' и g : M → F' гладкие до степени n, то x ↦ (f(x), g(x)) гладко отображается в произведение E' × F'.

LaTeX

$$ContMDiffWithinAt I 𝓘(𝕜,E') n f s x ∧ ContMDiffWithinAt I 𝓘(𝕜,F') n g s x ⇒ ContMDiffWithinAt I 𝓘(𝕜, E'×F') n (\lambda x, (f x, g x)) s x$$

Lean4

theorem prodMk_space {f : M → E'} {g : M → F'} (hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x)
    (hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x) : ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) s x :=
  by
  rw [contMDiffWithinAt_iff] at *
  exact ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

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