hasDerivAt

Mathlib.Analysis.Calculus.Deriv.Linear

URI: https://scilib.ai/kg/mathlib#LinearMap.hasDerivAt

English

For e: 𝕜 →ₗ[𝕜] F, HasDerivAt e (e 1) x holds for every x; i.e., the derivative of the map x ↦ e x is the constant e(1).

Русский

Для e: 𝕜 →ₗ[𝕜] F имеет место HasDerivAt e (e 1) в любой точке; производная константна и равна e(1).

LaTeX

$$$\\text{HasDerivAt} (\\lambda x, e x) (e(1)) \\, x$$$

Lean4

protected theorem hasDerivAt : HasDerivAt e (e 1) x :=
  e.hasDerivAtFilter

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru