inversion — Mathlib

English

If c and R vary continuously and x varies continuously with the property x(a) ≠ c(a), then the map a ↦ inversion(c(a), R(a), x(a)) is continuous at a.

Русский

Если c и R непрерывно зависят, а x зависит непрерывно и соблюдается x(a) ≠ c(a), то a ↦ inversion(c(a), R(a), x(a)) непрерывно в a.

LaTeX

$$$(c,R,x)\text{ continuous with } x(a)\neq c(a)\Rightarrow a\mapsto inversion(c(a),R(a),x(a)) \text{ continuous at } a$$$

Lean4

protected theorem inversion (hc : Continuous c) (hR : Continuous R) (hx : Continuous x) (hne : ∀ a, x a ≠ c a) :
    Continuous (fun a ↦ inversion (c a) (R a) (x a)) :=
  continuous_iff_continuousAt.2 fun _ ↦ hc.continuousAt.inversion hR.continuousAt hx.continuousAt (hne _)

Похожие утверждения