hasDerivAt_neg

Mathlib.Analysis.Calculus.Deriv.Add

URI: https://scilib.ai/kg/mathlib#hasDerivAt_neg

English

The derivative of the negation map at a point x equals −1; i.e., (-id)'(x) = −1.

Русский

Производная отображения отрицания в точке x равна −1; то есть (-id)'(x) = −1.

LaTeX

$$$ (-\mathrm{id})'(x) = -1 $$$

Lean4

theorem hasDerivAt_neg : HasDerivAt Neg.neg (-1) x :=
  hasDerivAtFilter_neg _ _

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

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

Разделы

Аффилиация

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