hasDerivAt_neg'

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative of the negation at x is −1; i.e., the slope is −1.

Русский

Производная отрицания в точке x равна −1; то есть наклон равен −1.

LaTeX

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

Lean4

theorem hasDerivAt_neg' : HasDerivAt (fun x ↦ -x) (-1) x :=
  hasDerivAtFilter_neg _ _

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

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

Разделы

Аффилиация

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