prodMk — Mathlib

English

If f and g are C^n in the model-space context, then the product map is C^n into the product model-space.

Русский

Если две карты гладкие в контексте модели, то их произведение также гладко в произведении моделей.

LaTeX

$$ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n f s x → ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n g s x → ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (Prod E' F')) n (\lambda x, { fst := f x, snd := g x }) s x$$

Lean4

nonrec theorem prodMk {f : M → M'} {g : M → N'} (hf : ContMDiffAt I I' n f x) (hg : ContMDiffAt I J' n g x) :
    ContMDiffAt I (I'.prod J') n (fun x => (f x, g x)) x :=
  hf.prodMk hg

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