English
If f is ContDiffWithinAt 𝕜 n at p.1 on s and g is ContDiffWithinAt 𝕜 n at p.2 on t, then the product map Prod.map f g is ContDiffWithinAt 𝕜 n on s×ˢt at p.
Русский
Если f имеет показатель ContDiffWithinAt 𝕜 n в точке p.1 на множестве s, и g имеет показатель ContDiffWithinAt 𝕜 n в точке p.2 на mножестве t, тогда отображение Prod.map f g в точке p на паре (p.1,p.2) является ContDiffWithinAt 𝕜 n на произведении множеств.
LaTeX
$$$\\forall s,t\\ f,g,p\\;\\big(\\mathrm{hf}:\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ f\\ s\\ p.1\\big)\\to\\big(\\mathrm{hg}:\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ g\\ t\\ p.2\\big)\\to\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\big(\\mathrm{Prod.map}\\ f\\ g\\big)\\ (s\\timesˢ t)\\ p$$$
Lean4
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point. -/
@[fun_prop]
theorem prodMap' {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffWithinAt 𝕜 n f s p.1)
(hg : ContDiffWithinAt 𝕜 n g t p.2) : ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p :=
(hf.comp p contDiffWithinAt_fst (prod_subset_preimage_fst _ _)).prodMk
(hg.comp p contDiffWithinAt_snd (prod_subset_preimage_snd _ _))
