inverse — Mathlib

English

If h is differentiable and h(x) is a unit for all x, then the inverse map is differentiable with the stated derivative at each point.

Русский

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

LaTeX

$$$$\forall x, \; \text{DifferentiableAt } (h(x)^{-1}) = -h(x)^{-1} Dh(x) h(x)^{-1}$$$$

Lean4

@[simp, fun_prop]
theorem inverse (hf : Differentiable 𝕜 h) (hz : ∀ x, IsUnit (h x)) : Differentiable 𝕜 fun x => Ring.inverse (h x) :=
  fun x => (hf x).inverse (hz x)

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