differentiableWithinAt_inverse — Mathlib

English

If x is a unit in a normed division ring R, then the function Inv.inv is differentiable at x with derivative -mulLeftRight 𝕜 R x^{-1} x^{-1}. The result is consistent with the nonunit case via hasFDerivAt_ringInverse.

Русский

Если x является единицей в нормированном деление кольце R, то Inv.inv дифференцируема в x, её производная равна -mulLeftRight 𝕜 R x^{-1} x^{-1}.

LaTeX

$$$\text{If } x \in R^{\times}, \; HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x^{-1} x^{-1}) x.$$$

Lean4

@[fun_prop]
theorem differentiableWithinAt_inverse {x : R} (hx : IsUnit x) (s : Set R) :
    DifferentiableWithinAt 𝕜 (@Ring.inverse R _) s x :=
  (differentiableAt_inverse hx).differentiableWithinAt

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