prodMap — Mathlib

English

If f is C^n smooth on a set s and g is C^n smooth on a set r, then the map (x,y) ↦ (f(x), g(y)) is C^n on the product set s × r.

Русский

Если f гладко(класс C^n) на множестве s и g гладко(класс C^n) на множестве r, то отображение (x, y) ↦ (f(x), g(y)) гладко класса C^n на произведении s × r.

LaTeX

$$$ (\ContMDiffOn I I' n f s) \land (\ContMDiffOn J J' n g r) \;\Rightarrow\; \ContMDiffOn (I.seg J) (I'.seg J') n (Prod.map f g) (s \times{\!\!} r) $$$

Lean4

theorem prodMap (hf : ContMDiffOn I I' n f s) (hg : ContMDiffOn J J' n g r) :
    ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) :=
  (hf.comp contMDiffOn_fst mapsTo_fst_prod).prodMk <| hg.comp contMDiffOn_snd mapsTo_snd_prod

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