curry_right — Mathlib

English

The product map of two C^n maps is C^n on the product set

Русский

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

LaTeX

$$$\\displaystyle \\operatorname{ContMDiffOn} \\; I \\; (I'.prod J') \\; n \\; (\\mathrm{Prod.map} \\; f \\; g) \\; (s \\times^\\! r) = \\cdots$$$

Lean4

/-- Curried `C^n` functions are `C^n` in the second coordinate. -/
theorem curry_right {f : M → M' → N} {x : M} {s : Set (M × M')} (fa : ContMDiffOn (I.prod I') J n (uncurry f) s) :
    ContMDiffOn I' J n (fun y ↦ f x y) {y | (x, y) ∈ s} := fun y m ↦ (fa (x, y) m).along_snd

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