prodMap — Mathlib

English

Currying preserves C^n in the second variable

Русский

Каррирование сохраняет C^n по второй переменной

LaTeX

$$$\\displaystyle \\text{curryRight: } \\text{ContMDiffWithinAt } (I.prod I') J n (\\mathrm{uncurry} f) \\Rightarrow \\text{ContMDiffWithinAt } I' J n (\\lambda y \\mapsto f x y)$$$

Lean4

theorem prodMap (hf : ContMDiffAt I I' n f x) (hg : ContMDiffAt J J' n g y) :
    ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y) :=
  by
  simp only [← contMDiffWithinAt_univ, ← univ_prod_univ] at *
  exact hf.prodMap hg

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