inversion — Mathlib

English

If c, R, x are differentiable maps, and x(a) ≠ c(a) for all a, then the inversion map a ↦ inversion(c(a), R(a), x(a)) is differentiable.

Русский

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

LaTeX

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

Lean4

protected theorem inversion (hc : Differentiable ℝ c) (hR : Differentiable ℝ R) (hx : Differentiable ℝ x)
    (hne : ∀ a, x a ≠ c a) : Differentiable ℝ (fun a ↦ inversion (c a) (R a) (x a)) := fun a ↦
  (hc a).inversion (hR a) (hx a) (hne a)

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