inversion — Mathlib

English

If c, R, x are differentiable (or differentiable on a set) with x(a) ≠ c(a), then the map a ↦ inversion(c(a), R(a), x(a)) is differentiable.

Русский

Если c, R и x дифференцируемы (на множестве), и x(a) ≠ c(a), то a ↦ inversion(c(a), R(a), x(a)) дифференцируема.

LaTeX

$$Differentiable(c) ∧ Differentiable(R) ∧ Differentiable(x) ∧ ∀ a, x(a) ≠ c(a) ⇒ Differentiable(a ↦ inversion(c(a), R(a), x(a)))$$

Lean4

protected nonrec theorem inversion (hc : ContDiff ℝ n c) (hR : ContDiff ℝ n R) (hx : ContDiff ℝ n x)
    (hne : ∀ a, x a ≠ c a) : ContDiff ℝ n (fun a ↦ inversion (c a) (R a) (x a)) :=
  contDiff_iff_contDiffAt.2 fun a ↦ hc.contDiffAt.inversion hR.contDiffAt hx.contDiffAt (hne a)

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