English
If h: M'×N'→N is C^n within at, and f,g: M→M',M→N' are C^n within at, then the map x↦h(f(x),g(x)) is C^n within at.
Русский
Если h: M'×N'→N гладко в пределах в точке y, а f,g: M→M',M→N' гладкие в точке x, то x↦h(f(x),g(x)) гладко в точке x.
LaTeX
$$$\\displaystyle \\text{If } h: M'\\times N'\\to N,\\; f: M\\to M',\\; g: M\\to N' \\\\text{and}\\\\ ha: ContMDiffWithinAt( I'.prod J') J n h t (f x, g x),\\; fa: ContMDiffWithinAt I I' n f s x,\\; ga: ContMDiffWithinAt I J' n g s x,\\; st:MapsTo(\\lambda x.(f x,g x)) s t, \\\\text{then } ContMDiffWithinAt I J n (\\lambda x. h (f x, g x)) s x.$$
Lean4
/-- `ContMDiffWithinAt.comp` for a function of two arguments. -/
theorem comp₂ {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} {t : Set (M' × N')}
(ha : ContMDiffWithinAt (I'.prod J') J n h t (f x, g x)) (fa : ContMDiffWithinAt I I' n f s x)
(ga : ContMDiffWithinAt I J' n g s x) (st : MapsTo (fun x ↦ (f x, g x)) s t) :
ContMDiffWithinAt I J n (fun x ↦ h (f x, g x)) s x :=
ha.comp (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga) st
