deriv_inv'' — Mathlib

English

Same as above: if differentiable at x and x ≠ 0, then derivative of inverse is − derivAt x / x^2.

Русский

Как выше: если дифференцируемо в x и x ≠ 0, тогда производная обратной функции − deriv x / x^2.

LaTeX

$$$\\text{If } hc: DifferentiableAt 𝕜 c x \\text{ and } hx: c x ≠ 0, \\text{ then } deriv (c^{-1}) x = - (deriv c x)/c x^2$$$

Lean4

@[simp]
theorem deriv_inv'' (hc : DifferentiableAt 𝕜 c x) (hx : c x ≠ 0) : deriv (c⁻¹) x = -deriv c x / c x ^ 2 :=
  (hc.hasDerivAt.inv hx).deriv

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