inversion — Mathlib

English

If c, R, x are ContDiffAt Real n at a and Ne (x(a)) (c(a)), then the map a ↦ inversion(c(a), R(a), x(a)) is ContDiffAt Real n at a.

Русский

Если c, R и x имеют ContDiffAt Real n в точке a и x(a) ≠ c(a), то a ↦ inversion(c(a), R(a), x(a)) имеет ContDiffAt Real n в a.

LaTeX

$$$\text{ContDiffAt}(Real,n,c,a) \land \text{ContDiffAt}(Real,n,R,a) \land \text{ContDiffAt}(Real,n,x,a) \land Ne(x(a), c(a)) \Rightarrow \text{ContDiffAt}(Real,n, a\mapsto inversion(c(a),R(a),x(a)), a)$$$

Lean4

protected nonrec theorem inversion (hc : ContDiffAt ℝ n c a) (hR : ContDiffAt ℝ n R a) (hx : ContDiffAt ℝ n x a)
    (hne : x a ≠ c a) : ContDiffAt ℝ n (fun a ↦ inversion (c a) (R a) (x a)) a :=
  hc.inversion hR hx hne

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