English
Variant of the WithinAt prodMap' lemma: if hf and hg are MDifferentiableWithinAt at p.1 and p.2, then the product map is differentiable within at p.
Русский
Вариант леммы WithinAt: если hf и hg дифференцируемы внутри на соответствующих координатах, то произведение дифференцируемо.
LaTeX
$$$\forall p=(p_1,p_2) \in M×N, \; hf: MDifferentiableWithinAt I I' f s p_1, \; hg: MDifferentiableWithinAt J J' g r p_2 \Rightarrow MDifferentiableWithinAt (I.prod J) (I'.prod J') (\mathrm{Prod.map} f g) (s ×ˢ r) p$$$
Lean4
/-- Variant of `MDifferentiableAt.prod_map` in which the point in the product is given as `p`
instead of a pair `(x, y)`. -/
theorem prodMap' {p : M × N} (hf : MDifferentiableAt I I' f p.1) (hg : MDifferentiableAt J J' g p.2) :
MDifferentiableAt (I.prod J) (I'.prod J') (Prod.map f g) p :=
hf.prodMap hg
