English
If hf and hg are ContDiffWithinAt 𝕜 n for f and g at p and q respectively, then Prod.map f g is ContDiffWithinAt 𝕜 n at (p,q) on s×t.
Русский
Если f и g оба являются ContDiffWithinAt 𝕜 n на точках p и q соответственно, то Prod.map f g является ContDiffWithinAt 𝕜 n на паре (p,q) в произведении множеств.
LaTeX
$$$\\forall s,t\\ f,g\\ p\\ q,\\; hf:\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ f\\ s\\ p \\to hg: \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ g\\ t\\ q \\Rightarrow\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ (\\mathrm{Prod.map}\\ f\\ g)\\ (s×ˢ t)\\ (p,q)$$$
Lean4
@[fun_prop]
theorem prodMap {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'} {x : E} {y : E'} (hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g t y) : ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y) :=
ContDiffWithinAt.prodMap' hf hg
