English
If c, R, x are differentiable within a set s and x(a) ≠ c(a) for all a ∈ s, then a ↦ inversion(c(a), R(a), x(a)) is differentiable on s.
Русский
Если c, R и x дифференцируемы внутри множества s и для всех a ∈ s выполняется x(a) ≠ c(a), то а ↦ inversion(c(a), R(a), x(a)) дифференцируема на s.
LaTeX
$$$\text{DifferentiableWithinAt}(Real,c,s) ∧ \text{DifferentiableWithinAt}(Real,R,s) ∧ \text{DifferentiableWithinAt}(Real,x,s) ∧ \forall a\in s, x(a) \ne c(a) \Rightarrow \text{DifferentiableWithinAt}(Real, a\mapsto inversion(c(a),R(a),x(a)), s)$$$
Lean4
protected theorem inversion (hc : DifferentiableWithinAt ℝ c s a) (hR : DifferentiableWithinAt ℝ R s a)
(hx : DifferentiableWithinAt ℝ x s a) (hne : x a ≠ c a) :
DifferentiableWithinAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) s a :=
-- TODO: Use `.div` https://github.com/leanprover-community/mathlib4/issues/5870
(((hR.mul <| (hx.dist ℝ hc hne).inv (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc
