hasDerivAt_inv

Mathlib.Analysis.Calculus.Deriv.Inv

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

English

If x ≠ 0, the derivative of x ↦ x^{-1} at x is -(x^2)^{-1}.

Русский

Если x ≠ 0, производная x ↦ x^{-1} в точке x равна -(x^2)^{-1}.

LaTeX

$$$$HasDerivAt\ (\lambda y, y^{-1})\ (-(x^2)^{-1})\ x\quad (x \neq 0)$$$$

Lean4

theorem hasDerivAt_inv (x_ne_zero : x ≠ 0) : HasDerivAt (fun y => y⁻¹) (-(x ^ 2)⁻¹) x :=
  (hasStrictDerivAt_inv x_ne_zero).hasDerivAt

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

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

Разделы

Аффилиация

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