mdifferentiableWithinAt_snd — Mathlib

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

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