prodMap' — Mathlib

English

The map assigning nested products is smooth in the product coordinates

Русский

Схема вложенных произведений гладкая в координатах произведения

LaTeX

$$$\\displaystyle \\text{Prod.map} \\; (\\mathrm{fst}, \\mathrm{snd}) = \\mathrm{prod}\;\\;\\text{smooth}$$$

Lean4

/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
theorem prodMap' {p : M × N} (hf : ContMDiffWithinAt I I' n f s p.1) (hg : ContMDiffWithinAt J J' n g r p.2) :
    ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) p :=
  (hf.comp p contMDiffWithinAt_fst mapsTo_fst_prod).prodMk <| hg.comp p contMDiffWithinAt_snd mapsTo_snd_prod

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