lineDeriv_zero — Mathlib

English

Let f: E → F be a function between normed spaces over a nontrivial normed field 𝕜. Then the line derivative of f at x in the zero direction is zero: lineDeriv 𝕜 f x 0 = 0.

Русский

Пусть f: E → F — функция между нормированными пространствами над ненулевым нормированным полем 𝕜. Тогда линейная производная вдоль направления 0 в точке x равна 0: lineDeriv 𝕜 f x 0 = 0.

LaTeX

$$$$ \operatorname{lineDeriv}_{\mathbb{K}} f x 0 = 0 $$$$

Lean4

theorem lineDeriv_zero : lineDeriv 𝕜 f x 0 = 0 :=
  hasLineDerivAt_zero.lineDeriv

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