English
The product map of a nested product is C^n: mapping ((M×M')×N) to M×(M'×N) via (x,y,z)↦(x, y, z) is ContMDiff.
Русский
Произведение карт перехода для тройного произведения сохраняет гладкость: отображение ((M×M')×N) → M×(M'×N) является C^n.
LaTeX
$$$\\operatorname{ContMDiff} ((I.\\text{prod} I').prod J) (I.\\text{prod} (I'.\\text{prod} J)) n \\; (x,y,z) \\mapsto (x_1, x_2, x_3)$$$
Lean4
/-- `ContMDiffAt.comp` for a function of two arguments. -/
theorem comp₂ {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M} (ha : ContMDiffAt (I'.prod J') J n h (f x, g x))
(fa : ContMDiffAt I I' n f x) (ga : ContMDiffAt I J' n g x) : ContMDiffAt I J n (fun x ↦ h (f x, g x)) x :=
ha.comp (f := fun x ↦ (f x, g x)) _ (fa.prodMk ga)
