hasFDerivWithinAt_inv — Mathlib

English

If x ≠ 0, then HasFDerivWithinAt (t ↦ t^{-1}) s x holds with the same linear map as HasFDerivAt, provided the same derivative value applies within s.

Русский

Если x ≠ 0, существует HasFDerivWithinAt для t ↦ t^{-1} внутри s в точке x, с тем же линейным отображением, что и в точке outside.

LaTeX

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

Lean4

theorem hasFDerivWithinAt_inv (x_ne_zero : x ≠ 0) :
    HasFDerivWithinAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) s x :=
  (hasFDerivAt_inv x_ne_zero).hasFDerivWithinAt

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