English
Let 𝕜 be a nontrivial normed field, s a subset of 𝕜, and x ∈ 𝕜 with x ≠ 0 and x is a point of unique differentiability within s. Then the derivative within s at x of the reciprocal map t ↦ t^{-1} equals −(x^2)^{−1}. In other words, derivWithin (t ↦ t^{-1}) s x = −(x^2)^{−1}.
Русский
Пусть 𝕜 — ненулевая нормированная полная линейная алгебра, s — подмножество 𝕜, x ∈ 𝕜, x ≠ 0, и x является точкой уникальной дифференцируемости в пределах s. Тогда производная внутри множества s от отображения x ↦ x^{-1} в точке x равна −(x^2)^{−1}. Иными словами, derivWithin (t ↦ t^{-1}) s x = −(x^2)^{−1}.
LaTeX
$$$\\forall 𝕜 [NontriviallyNormedField 𝕜], \\forall x \\in 𝕜, \\forall s \\subseteq 𝕜, [x \\ne 0] \\land UniqueDiffWithinAt 𝕜 s x \\Rightarrow \\operatorname{derivWithin}_{s}(t \\mapsto t^{-1})(x) = -(x^2)^{-1}$$$
Lean4
theorem derivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹ :=
by
rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]
exact deriv_inv
