inv — Mathlib

English

If h is differentiable on a set S and h(x) ≠ 0 for all x in S, then the inverse function h⁻¹ is differentiable on S.

Русский

Если h дифференцируема на множества S и для каждого x ∈ S выполнено h(x) ≠ 0, то обратная функция h⁻¹ дифференцируема на S.

LaTeX

$$$\text{DifferentiableOn } 𝕜\ h\ S \rightarrow\text{DifferentiableOn } 𝕜\ h^{-1}\ S\quad\text{when } \forall x \in S,\ h(x) \neq 0$$$

Lean4

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

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