English
Suppose c, R, x are parameterized maps with c(a) → c, R(a) → R, x(a) → x as a approaches a₀, and x(a) ≠ c(a) for all a. Then the family a ↦ inversion(c(a), R(a), x(a)) tends to inversion(c, R, x) in the neighborhood of a₀.
Русский
Пусть параметры c(a), R(a), x(a) сходятся к c, R и x соответственно, и для всех a выполняется x(a) ≠ c(a). Тогда a↦inversion(c(a),R(a),x(a)) сходится к inversion(c,R,x) в окрестности a₀.
LaTeX
$$$\text{If } c(a)\to c,\; R(a)\to R,\; x(a)\to x,\; x(a)\neq c(a), \text{ then } inversion(c(a),R(a),x(a)) \to inversion(c,R,x)$$$
Lean4
protected nonrec theorem inversion (hc : ContinuousAt c a₀) (hR : ContinuousAt R a₀) (hx : ContinuousAt x a₀)
(hne : x a₀ ≠ c a₀) : ContinuousAt (fun a ↦ inversion (c a) (R a) (x a)) a₀ :=
hc.inversion hR hx hne
