English
The product map of two C^n functions is C^n within at if the component functions are C^n within at.
Русский
Произведение двух C^n-функций является C^n внутри при условии гладкости каждой функции.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffWithinAt} \\; I \\; I' \\; n \\; f \\; s \\; p.1 \\land \\operatorname{ContMDiffWithinAt} \\; J \\; J' \\; n \\; g \\; r \\; p.2 \\Rightarrow \\operatorname{ContMDiffWithinAt} \\; (I.\\mathrm{prod} J) \\; (I'.\\mathrmprod J') \\; n \\; (\\mathrm{Prod.map} \\\\ f \\\\ g) \\; (s \\times r) \\; p$$
Lean4
/-- Curried `C^n` functions are `C^n` in the second coordinate. -/
theorem curry_right {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')}
(fa : ContMDiffWithinAt (I.prod I') J n (uncurry f) s (x, y)) :
ContMDiffWithinAt I' J n (fun y ↦ f x y) {y | (x, y) ∈ s} y :=
fa.comp₂ contMDiffWithinAt_const contMDiffWithinAt_id (fun _ h ↦ h)
