English
There exists HasMFDerivAt for Prod.snd with the expected continuous linear map as derivative: HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)).
Русский
Существует HasMFDerivAt для Prod.snd с ожидаемой производной: непрерывно-линейное отображение snd между касательными пространствами.
LaTeX
$$$ HasMFDerivAt (I\prod I') I' Prod.snd x (\, ContinuousLinearMap.snd\; 𝕜\; (\mathrm{TangentSpace}\; I\, x.1) (\mathrm{TangentSpace}\; I'\, x.2)\,)$$$
Lean4
theorem mdifferentiableWithinAt_snd {s : Set (M × M')} {x : M × M'} :
MDifferentiableWithinAt (I.prod I') I' Prod.snd s x :=
mdifferentiableAt_snd.mdifferentiableWithinAt