mdifferentiableAt_snd — Mathlib

English

The MF-derivative of Prod.snd is the snd-linear map between tangent spaces: mfderiv (I.prod I') I' Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2).

Русский

Производная MF от Prod.snd равна линейному отображению snd между касательными пространствами.

LaTeX

$$$mfderiv (I\prod I')\, I'\, Prod.snd\, x = \mathrm{ContinuousLinearMap.snd}\; 𝕜\; (\mathrm{TangentSpace}\; I\, x.1)\; (\mathrm{TangentSpace}\; I'\, x.2)$$$

Lean4

theorem mdifferentiableAt_snd {x : M × M'} : MDifferentiableAt (I.prod I') I' Prod.snd x :=
  (hasMFDerivAt_snd x).mdifferentiableAt

Похожие утверждения