prodMap — Mathlib

English

If hf is ContMDiff on I→I' and hg is ContMDiff on J→J' without specifying domains, then the product map Prod.map f g is ContMDiff from I×J to I'×J'.

Русский

Если hf и hg являются ContMDiff отображениями f и g соответствующе на пространствах I и J, то произведение Prod.map f g гладко класса C^n на пространстве I×J в I'×J'.

LaTeX

$$$ (\ContMDiff I I' n f) \land (\ContMDiff J J' n g) \Rightarrow \ContMDiff (I.seg J) (I'.seg J') n (Prod.map f g) $$$

Lean4

theorem prodMap (hf : ContMDiff I I' n f) (hg : ContMDiff J J' n g) :
    ContMDiff (I.prod J) (I'.prod J') n (Prod.map f g) :=
  by
  intro p
  exact (hf p.1).prodMap' (hg p.2)

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