hasDerivWithinAt_inv — Mathlib

English

If x ≠ 0, the derivative within s of the inverse map x ↦ x^{-1} at x is -(x^2)^{-1}.

Русский

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

LaTeX

$$$$HasDerivWithinAt\ (\lambda y, y^{-1})\ (-(x^2)^{-1})\ s\ x\quad (x \neq 0)$$$$

Lean4

theorem hasDerivWithinAt_inv (x_ne_zero : x ≠ 0) (s : Set 𝕜) : HasDerivWithinAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) s x :=
  (hasDerivAt_inv x_ne_zero).hasDerivWithinAt

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