fderiv_single — Mathlib

English

The Fréchet derivative of the Pi.single i map is the i-th projection; i.e., fderiv Pi.single i equals Pi.single i applied to id.

Русский

Производная отображения Pi.single i равна i-й проекции; fderiv Pi.single i = Pi.single i ∘ id.

LaTeX

$$$\\mathrm{fderiv}(\\Pi\\text{.single } i) = \\pi\\bigl(\\Pi\\text{.single } i (\\mathrm{id}_{\\mathbb{K}})\\bigr)$$$

Lean4

theorem fderiv_single {i : ι} (y : E i) : fderiv 𝕜 (Pi.single i) y = .pi (Pi.single i (.id 𝕜 (E i))) :=
  fderiv_update 0 y

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