fun_inv — Mathlib

English

If h is differentiableOn S and h(x) ≠ 0 for every x ∈ S, then the function x ↦ (h(x))^{-1} is differentiableOn S.

Русский

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

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{K}}(h^{-1},S)$ given $\\text{DifferentiableOn}_{\\mathbb{K}}(h,S)$ and $\\forall x \\in S,\\ h(x) \\neq 0$$$

Lean4

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

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