deriv_inv — Mathlib

English

The derivative of the reciprocal function is -(x^2)^{-1} for x ≠ 0; at x = 0 the derivative does not exist.

Русский

Производная функции обратного равна -(x^2)^{-1} при x ≠ 0; при x = 0 производная не существует.

LaTeX

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

Lean4

theorem deriv_inv : deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹ :=
  by
  rcases eq_or_ne x 0 with (rfl | hne)
  · simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
  · exact (hasDerivAt_inv hne).deriv

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