inverse — Mathlib

English

If h is differentiable on a set and IsUnit(h x) for all x in the set, then the map x ↦ h(x)^{-1} is differentiable on that set.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem inverse (hf : DifferentiableWithinAt 𝕜 h S z) (hz : IsUnit (h z)) :
    DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z :=
  (differentiableAt_inverse hz).comp_differentiableWithinAt z hf

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