English
If x ≠ 0 and hxs holds (UniqueDiffWithinAt 𝕜 s x), then fderivWithin 𝕜 (t ↦ t^{-1}) s x equals smulRight 1 (-(x^2)^{-1}).
Русский
Пусть x ≠ 0 и UniqueDiffWithinAt 𝕜 s x, тогда fderivWithin 𝕜 (t ↦ t^{-1}) s x равен smulRight 1 (−(x^2)^{-1}).
LaTeX
$$$\\forall 𝕜 [NontriviallyNormedField 𝕜], x \\ne 0, hxs : UniqueDiffWithinAt 𝕜 s x \\Rightarrow fderivWithin 𝕜 (\\lambda t. t^{-1}) s x = smulRight (1 : 𝕜 \\toL[𝕜] 𝕜) (-(x^2)^{-1})$$$
Lean4
theorem fderivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) :=
by
rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]
exact fderiv_inv
