prodMap' — Mathlib

English

The product map of two C^n At maps is C^n at the product point

Русский

Произведение двух C^n в точке является C^n в произведённой точке

LaTeX

$$$\\displaystyle \\operatorname{ContMDiffAt} \\; I \\; (I'.prod J') \\; n \\; (\\mathrm{Prod.map} \\; f \\; g) \\; (x,y)$$$

Lean4

theorem prodMap' {p : M × N} (hf : ContMDiffAt I I' n f p.1) (hg : ContMDiffAt J J' n g p.2) :
    ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p :=
  hf.prodMap hg

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