curry_left — Mathlib

English

If f: M → M' and g: M → N' are C^n at x, then the product map x ↦ (f x, g x) is C^n at (x,y).

Русский

Если f и g — C^n в точке x, то отображение x ↦ (f x, g x) —C^n в точке (x,y).

LaTeX

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

Lean4

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

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