prodMk — Mathlib

English

If f : M → M' and g : M → N' are ContMDiffWithinAt on a set s at x, then the pair map x ↦ (f(x), g(x)) is ContMDiffWithinAt with the product structure.

Русский

Если f : M → M' и g : M → N' являются ContMDiffWithinAt на области s вокруг x, то отображение x ↦ (f(x), g(x)) гладко в произведении.

LaTeX

$$$ContMDiffWithinAt I I' n f s x \wedge ContMDiffWithinAt I J' n g s x \Rightarrow ContMDiffWithinAt I (I'.prod J') n (\lambda x, (f x, g x)) s x$$

Lean4

theorem prodMk {f : M → M'} {g : M → N'} (hf : ContMDiffWithinAt I I' n f s x) (hg : ContMDiffWithinAt I J' n g s x) :
    ContMDiffWithinAt I (I'.prod J') 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⟩

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