hasDerivAt_update — Mathlib

English

In a finite index set, the update map HasDerivAt equals a derivative at every y with Pi.single i 1.

Русский

Для конечного множества индексов карта обновления имеет производную в каждой точке, равную единичному вектору.

LaTeX

$$$hasDerivAt_update\$x,i,y\$ : HasDerivAt\$Function.update x i\$\$Pi.single i (1 : 𝕜)\$ y$$$

Lean4

theorem hasDerivAt_update (x : ι → 𝕜) (i : ι) (y : 𝕜) : HasDerivAt (Function.update x i) (Pi.single i (1 : 𝕜)) y :=
  by
  convert (hasFDerivAt_update x y).hasDerivAt
  ext z j
  rw [Pi.single, Function.update_apply]
  split_ifs with h
  · simp [h]
  · simp [Pi.single_eq_of_ne h]

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