hasStrictDerivAt

Mathlib.Analysis.Calculus.Deriv.Linear

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

English

If a linear map e is differentiable, its derivative is e(1).

Русский

Если линейное отображение e дифференцируемо, производная равна e(1).

LaTeX

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

Lean4

protected theorem hasStrictDerivAt : HasStrictDerivAt e (e 1) x :=
  e.hasStrictFDerivAt.hasStrictDerivAt

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

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

Разделы

Аффилиация

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