𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹
rw [DifferentiableAt.derivWithin (differentiableAt_inv.2 x_ne_zero) hxs]
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
exact deriv_inv