derivWithin_inv' — Mathlib

English

Equivalent form: derivWithin (c^{-1}) s x = - derivWithin c s x / c x^2 under the usual differentiability conditions.

Русский

Эквивалентная форма: derivWithin (c^{-1}) s x = - derivWithin c s x / c x^2 при обычных условиях дифференцируемости.

LaTeX

$$$ derivWithin (c^{-1}) s x = -\\dfrac{derivWithin c s x}{c x^2}$, under differentiability hypotheses.$$

Lean4

theorem derivWithin_inv' (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0) :
    derivWithin (c⁻¹) s x = -derivWithin c s x / c x ^ 2 :=
  derivWithin_fun_inv' hc hx

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