English
If hf and hg are MDifferentiableWithinAt on s and r respectively, then Prod.map f g is MDifferentiableWithinAt on s×r.
Русский
Если hf и hg дифференцируемы внутри на s и r соответственно, то Prod.map f g дифференцируемо внутри на s×r.
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 ×ˢ r) (x,y)$$$
Lean4
theorem mfderiv_prod_right {x₀ : M} {y₀ : M'} :
mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :=
by
refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
