fderiv_update — Mathlib

English

The derivative of the update map in the direction y equals the projection onto the i-th coordinate; i.e., fderiv update = projection.

Русский

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

LaTeX

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

Lean4

theorem fderiv_update (x : ∀ i, E i) {i : ι} (y : E i) :
    fderiv 𝕜 (Function.update x i) y = .pi (Pi.single i (.id 𝕜 (E i))) :=
  (hasFDerivAt_update x y).fderiv

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