inv — Mathlib

English

If h is differentiableAt z and h(z) ≠ 0, then the map x ↦ h(x)^{-1} has differentiableWith respect to z (i.e., the derivative exists).

Русский

Если h дифференцируема в точке z и h(z) ≠ 0, то x ↦ h(x)^{-1} дифференцируема в z.

LaTeX

$$$\\text{DifferentiableAt}_{\\mathbb{K}}(h^{-1}, z)$ given $\\text{DifferentiableAt}_{\\mathbb{K}}(h, z)$ and $h(z) \\neq 0$$$

Lean4

@[simp, fun_prop]
theorem inv (hf : Differentiable 𝕜 h) (hz : ∀ x, h x ≠ 0) : Differentiable 𝕜 (h⁻¹) := fun x => (hf x).inv (hz x)

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