deriv_inv'

Mathlib.Analysis.Calculus.Deriv.Inv

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

English

The derivative of the inverse map is identically -(x^2)^{-1} as a function of x.

Русский

Производная обратной функции тождественно равна -(x^2)^{-1}.

LaTeX

$$$$\operatorname{deriv}(x \mapsto x^{-1}) = -(x^2)^{-1}.$$$$

Lean4

@[simp]
theorem deriv_inv' : (deriv fun x : 𝕜 => x⁻¹) = fun x => -(x ^ 2)⁻¹ :=
  funext fun _ => deriv_inv

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

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

Разделы

Аффилиация

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