inv — Mathlib

English

If h is differentiable within at S at z and h(z) ≠ 0, then h^{-1} is differentiable within at S at z.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem inv (hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) : DifferentiableWithinAt 𝕜 (h⁻¹) S z :=
  (differentiableAt_inv hz).comp_differentiableWithinAt z hf

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