English
If c, R, and x vary continuously (with x(a) ≠ c(a) for all a in the domain), then the composed map a ↦ inversion(c(a), R(a), x(a)) is continuous at the point a.
Русский
Если центрация c, радиус R и точка x изменяются непрерывно так, что x(a) ≠ c(a) для всех a в области, то отображение a ↦ inversion(c(a), R(a), x(a)) непрерывно в точке a.
LaTeX
$$передаточная непрерывность: $\text{if } c, R, x \text{ are continuous, and } x(a)\neq c(a),\; a \mapsto inversion(c(a),R(a),x(a)) \text{ is continuous at } a$$$
Lean4
protected nonrec theorem inversion (hc : ContinuousWithinAt c s a₀) (hR : ContinuousWithinAt R s a₀)
(hx : ContinuousWithinAt x s a₀) (hne : x a₀ ≠ c a₀) :
ContinuousWithinAt (fun a ↦ inversion (c a) (R a) (x a)) s a₀ :=
hc.inversion hR hx hne
