English
The product map of two C^n functions on sets is C^n on the product set.
Русский
Произведение двух функций класса C^n на множествах является функцией класса C^n на произведении множеств.
LaTeX
$$$\\forall s,t\\ f,g,\\; \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ f\\ s\\ \\to\\ \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ g\\ t\\Rightarrow\\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ (\\mathrm{Prod.map}\\ f\\ g)\\ (s\\timesˢ t)$$$
Lean4
/-- The product map of two `C^n` functions on a set is `C^n` on the product set. -/
@[fun_prop]
theorem prodMap {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type*} [NormedAddCommGroup F']
[NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} (hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g t) : ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t) :=
(hf.comp contDiffOn_fst (prod_subset_preimage_fst _ _)).prodMk (hg.comp contDiffOn_snd (prod_subset_preimage_snd _ _))
