fun_inv — Mathlib

English

If h is differentiable within a set S at a point z and h(z) ≠ 0, then the function x ↦ (h(x))^{-1} is differentiable within S at z.

Русский

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

LaTeX

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

Lean4

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

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