prodMap — Mathlib

English

Currying preserves C^n in the first variable

Русский

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

LaTeX

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

Lean4

theorem prodMap (hf : ContMDiffWithinAt I I' n f s x) (hg : ContMDiffWithinAt J J' n g r y) :
    ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) (x, y) :=
  ContMDiffWithinAt.prodMap' hf hg

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