fun_inv — Mathlib

English

If h is differentiableWithinAt on S and h(z) ≠ 0, then (h)^{-1} is differentiableWithinAt on 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

@[simp, fun_prop]
theorem fun_inv (hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) : DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z :=
  (differentiableAt_inv hz).comp z hf

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