hasStrictDerivAt_neg

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The negation map has strict derivative −1 at x; i.e., HasStrictDerivAt (−id) (−1) x.

Русский

Отрицание имеет строгое производное −1 в точке x; то есть HasStrictDerivAt (−id) (−1) x.

LaTeX

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

Lean4

theorem hasStrictDerivAt_neg : HasStrictDerivAt Neg.neg (-1) x :=
  HasStrictDerivAt.neg <| hasStrictDerivAt_id _

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

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

Разделы

Аффилиация

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