English
Let p=(x,y) ∈ M×N. If f is MDifferentiableWithinAt I I' f s x and g is MDifferentiableWithinAt J J' g r y, then Prod.map f g is MDifferentiableWithinAt (I.prod J) (I'.prod J') on s×r at p.
Русский
Пусть p=(x,y) ∈ M×N. Если f дифференцируемо внутри At x и g дифференцируемо внутри At y, то Prod.map f g дифференцируемо внутри At на s×r в точке p.
LaTeX
$$${\text{MDifferentiableWithinAt } I I' f s x} \land {\text{MDifferentiableWithinAt } J J' g r y} \Rightarrow {\text{MDifferentiableWithinAt } (I.prod J) (I'.prod J') (\mathrm{Prod.map}\ f\ g) (s\timesˢ r) (x,y)}$$$
Lean4
theorem prodMap (hf : MDifferentiableWithinAt I I' f s x) (hg : MDifferentiableWithinAt J J' g r y) :
MDifferentiableWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) (x, y) :=
MDifferentiableWithinAt.prodMap' hf hg
