English
If c, R, x are ContDiffWithinAt Real n on s and x(a) ≠ c(a) on s, then the composition a ↦ inversion(c(a), R(a), x(a)) is ContDiffWithinAt Real n on s.
Русский
Если c, R и x имеют непрерывную производную внутри s, и для всех a∈s выполняется x(a) ≠ c(a), то a ↦ inversion(c(a), R(a), x(a)) имеет ContDiffWithinAt Real n на s.
LaTeX
$$$\text{ContDiffWithinAt}(Real,n,c,s) \land \text{ContDiffWithinAt}(Real,n,R,s) \land \text{ContDiffWithinAt}(Real,n,x,s) \land \forall a\in s, x(a) \ne c(a) \Rightarrow \text{ContDiffWithinAt}(Real,n, a\mapsto inversion(c(a),R(a),x(a)), s)$$$
Lean4
protected theorem inversion (hc : ContDiffWithinAt ℝ n c s a) (hR : ContDiffWithinAt ℝ n R s a)
(hx : ContDiffWithinAt ℝ n x s a) (hne : x a ≠ c a) :
ContDiffWithinAt ℝ n (fun a ↦ inversion (c a) (R a) (x a)) s a :=
(((hR.div (hx.dist ℝ hc hne) (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc
