hasStrictFDerivAt_inv — Mathlib

English

If x ≠ 0, the strict derivative at x of the reciprocal map x ↦ x^{-1} is given by the same linear map as the Fréchet derivative, namely multiplication by −(x^2)^{−1}.

Русский

Если x ≠ 0, строгая производная в точке x от x ↦ x^{-1} совпадает с линейным отображением умножения на −(x^2)^{−1}.

LaTeX

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

Lean4

theorem hasStrictFDerivAt_inv (x_ne_zero : x ≠ 0) :
    HasStrictFDerivAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) x :=
  hasStrictDerivAt_inv x_ne_zero

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