English
If fa is ContMDiffWithinAt for the uncurry of f in two variables, then fixing the second variable yields that the function x ↦ f x y is ContMDiffWithinAt.
Русский
Если fa — C^n для функции-курари uncurry f в двух аргументах, то фиксация второго аргумента даёт, что x ↦ f x y — C^n.
LaTeX
$$$\\displaystyle \\operatorname{ContMDiffWithinAt} \\\\ I \\\\ J \\\\ n \\\\ (\\mathrm{uncurry} f) \\\\ s \\{ y \\} \\implies \\operatorname{ContMDiffWithinAt} I J n (\\lambda x. f x y) \\{ (x,y) \\in s \\} x$$
Lean4
/-- `ContMDiffAt.comp₂`, with a separate argument for point equality. -/
theorem comp₂_of_eq {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {y : M' × N'}
(ha : ContMDiffAt (I'.prod J') J n h y) (fa : ContMDiffAt I I' n f x) (ga : ContMDiffAt I J' n g x)
(e : (f x, g x) = y) : ContMDiffAt I J n (fun x ↦ h (f x, g x)) x :=
by
rw [← e] at ha
exact ha.comp₂ fa ga
