English
If DifferentiableWithinAt c s x and c x ≠ 0, then derivWithin (c^{-1}) s x = - derivWithin c s x / c x^2, with a potential caveat if UniqueDiffWithinAt fails.
Русский
Если DifferentiableWithinAt c s x и c x ≠ 0, то derivWithin (c^{-1}) s x = −(derivWithin c s x)/c x^2, возможно с оговоркой при отсутствии UniqueDiffWithinAt.
LaTeX
$$$\\forall {c s x},\\ DifferentiableWithinAt 𝕜 c s x \\land c x \\ne 0 \\Rightarrow derivWithin (c^{-1}) s x = -\\frac{derivWithin c s x}{c x^2}$ (при отсутствии UniqueDiffWithinAt возможно другое равенство).$$
Lean4
theorem derivWithin_fun_inv' (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0) :
derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2 :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hc.hasDerivWithinAt.inv hx).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
