English
If f: M → F1 and g: N → F2 are differentiable within at sets s and r respectively, then the product map Prod.map f g: M × N → F1 × F2 is differentiable within at the product set s × r. The derivative is the product of the derivatives.
Русский
Пусть f и g дифференцируемы внутри соответственно на s и r; тогда отображение Prod.map f g: M×N → F1×F2 дифференцируемо внутри s×r, и его производная равна паре производных.
LaTeX
$$$\text{MDifferentiableWithinAt } I I' f\ s\ p.1 \land \text{MDifferentiableWithinAt } J J' g\ r\ p.2 \Rightarrow \text{MDifferentiableWithinAt } (I.prod J) (I'.prod J') (\mathrm{Prod.map}\ f\ g)\ (s\times^{\text{S}} r)\ 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. -/
theorem prodMap' {p : M × N} (hf : MDifferentiableWithinAt I I' f s p.1) (hg : MDifferentiableWithinAt J J' g r p.2) :
MDifferentiableWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) p :=
(hf.comp p mdifferentiableWithinAt_fst (prod_subset_preimage_fst _ _)).prodMk <|
hg.comp p mdifferentiableWithinAt_snd (prod_subset_preimage_snd _ _)
