hasFDerivAt_single — Mathlib

English

The Fréchet derivative of the update map at x in direction y is the projection onto the i-th coordinate; i.e., fderiv_update(x,y) equals the i-th projection.

Русский

Пусть производная обновления в направлении y равна проекции на i-ую координату.

LaTeX

$$$\\mathrm{fderiv}(\\mathrm{Function.update}\\, x\\, i)\\, y = \\pi_i(\\cdot)$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_single {i : ι} (y : E i) : HasFDerivAt (Pi.single i) (.pi (Pi.single i (.id 𝕜 (E i)))) y :=
  hasFDerivAt_update 0 y

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