curry_right — Mathlib

English

The product map for two C^n maps is C^n

Русский

Произведение двух C^n-функций гладко

LaTeX

$$$\\displaystyle \\operatorname{ContMDiffAt} \\; I \\; (I'.prod J') \\; n \\; (\\mathrm{Prod.map} \\; f \\; g) \\; (x,y) \\iff \\operatorname{ContMDiffAt} \\; I \\; I' \\; n \\; f \\; x \\land \\operatorname{ContMDiffAt} \\; J \\; J' \\; n \\; g \\; y$$

Lean4

/-- Curried `C^n` functions are `C^n` in the second coordinate. -/
theorem curry_right {f : M → M' → N} {x : M} {y : M'} (fa : ContMDiffAt (I.prod I') J n (uncurry f) (x, y)) :
    ContMDiffAt I' J n (fun y ↦ f x y) y :=
  fa.comp₂ contMDiffAt_const contMDiffAt_id

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