English
If c, R, x depend continuously on a and x(a) ≠ c(a) for all a in s, then a ↦ inversion(c(a), R(a), x(a)) is continuous within the set s at every a₀ in s.
Русский
Если c, R и x зависят непрерывно от a и для всех a∈s выполняется x(a) ≠ c(a), то a ↦ inversion(c(a),R(a),x(a)) непрерывно внутри s в точке a₀.
LaTeX
$$$\text{If } c,R,x \text{ are continuous on } s, \; x(a) \ne c(a) \; \forall a\in s, \; a_0\in s, \; \\ (\text{then})\; inversion(c(a),R(a),x(a)) \text{ is continuous on } s \text{ at } a_0$$$
Lean4
protected theorem inversion (hc : ContinuousOn c s) (hR : ContinuousOn R s) (hx : ContinuousOn x s)
(hne : ∀ a ∈ s, x a ≠ c a) : ContinuousOn (fun a ↦ inversion (c a) (R a) (x a)) s := fun a ha ↦
(hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)
