deriv_fun_inv'' — Mathlib

English

Let hc be differentiable at x with hx ≠ 0; then the derivative of the inverse function is given by − deriv c x / c x^2.

Русский

Пусть hc — дифференцируемо в x, x ≠ 0; тогда производная обратной функции равна − deriv c x / c x^2.

LaTeX

$$$\\forall {𝕜} [NontriviallyNormedField 𝕜],{x},{c}: HasDerivAt c c' x \\Rightarrow c x ≠ 0 \\, \\Rightarrow \\, deriv (c^{-1}) x = - (deriv c x)/c x^2$$$

Lean4

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

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