inversion — Mathlib

English

If c, R, x are differentiable at a and x(a) ≠ c(a) then the function a ↦ inversion(c(a), R(a), x(a)) is differentiable at a.

Русский

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

LaTeX

$$DifferentiableAt Real c a ∧ DifferentiableAt Real R a ∧ DifferentiableAt Real x a ∧ Ne(x(a), c(a)) ⇒ DifferentiableAt Real (a ↦ inversion (c a) (R a) (x a)) a$$

Lean4

protected theorem inversion (hc : DifferentiableAt ℝ c a) (hR : DifferentiableAt ℝ R a) (hx : DifferentiableAt ℝ x a)
    (hne : x a ≠ c a) : DifferentiableAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) a :=
  by
  rw [← differentiableWithinAt_univ] at *
  exact hc.inversion hR hx hne

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