curry_right — Mathlib

English

The product map of two C^n functions is ContMDiff

Русский

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

LaTeX

$$$\\displaystyle \\operatorname{ContMDiff} \\; \\mathrm{Prod.map} \\; f \\; g = \\text{ContMDiff}(f,g)$$$

Lean4

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

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