hasDerivAt_single — Mathlib

English

The derivative of the single-coordinate map equals the corresponding unit vector.

Русский

Производная карты, выбирающей одну координату, равна соответствующему единичному вектору.

LaTeX

$$$deriv\\left(\\text{Pi.single } i\\right) y = \\Pi.single i 1$$$

Lean4

theorem hasDerivAt_single (i : ι) (y : 𝕜) : HasDerivAt (Pi.single (M := fun _ ↦ 𝕜) i) (Pi.single i (1 : 𝕜)) y :=
  hasDerivAt_update 0 i y

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