fderiv_inv — Mathlib

English

For x ≠ 0, the derivative at x of the map t ↦ t^{-1} is given by the linear map h ↦ −h/x^2; equivalently, f'(x) = −(x^2)^{-1} times the identity.

Русский

Для x ≠ 0 производная в точке x от t ↦ t^{-1} равна линейному отображению h ↦ −h/x^2; эквивалентно f'(x) = −(x^2)^{-1} умножение на единичное отображение.

LaTeX

$$$\\forall 𝕜 [NontriviallyNormedField 𝕜], x \\ne 0 \\Rightarrow fderiv 𝕜 (\\lambda t. t^{-1}) x = smulRight (1 : 𝕜 \\toL[𝕜] 𝕜) (-(x^2)^{-1})$$$

Lean4

theorem fderiv_inv : fderiv 𝕜 (fun x => x⁻¹) x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) := by
  rw [← deriv_fderiv, deriv_inv]

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