deriv

Mathlib.Analysis.Calculus.Deriv.Linear

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.deriv

English

The derivative of a continuous linear map evaluated at a point equals its action on 1.

Русский

Производная непрерывного линейного отображения в точке равна его действию на единицу.

LaTeX

$$$ \\mathrm{deriv} (\\mathrm{ContinuousLinearMap}.co e) x = e(1) $$$

Lean4

@[simp]
protected theorem deriv : deriv e x = e 1 :=
  e.hasDerivAt.deriv

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

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

Разделы

Аффилиация

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