inverse — Mathlib

English

If h is differentiable on S and IsUnit for all x ∈ S, then the map x ↦ h(x)^{-1} is differentiable on S.

Русский

Если h дифференцируема на S и для всех x ∈ S h(x) единично обратимо, тогда x ↦ h(x)^{-1} дифференцируема на S.

LaTeX

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

Lean4

@[simp, fun_prop]
theorem inverse (hf : DifferentiableAt 𝕜 h z) (hz : IsUnit (h z)) :
    DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z :=
  (differentiableAt_inverse hz).comp z hf

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