differentiableOn_inverse — Mathlib

English

If h is differentiable on a set and h(x) is a unit for all x in the set, then the map x ↦ h(x)^{-1} is differentiable on that set with derivative given pointwise by the inverse-derivative formula.

Русский

Если h дифференцируема на множестве и для всех x из множества h(x) является единицей, то x ↦ h(x)^{-1} дифференцируема на этом множестве с производной, заданной точечно формулой для обратной функции.

LaTeX

$$$\text{DifferentiableOn } 𝕜 (\lambda x, (h(x))^{-1}) S$ under IsUnit (h x).$$

Lean4

@[fun_prop]
theorem differentiableOn_inverse : DifferentiableOn 𝕜 (@Ring.inverse R _) {x | IsUnit x} := fun _x hx =>
  differentiableWithinAt_inverse hx _

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