localInverse — Mathlib

English

In one dimension, a local inverse g exists with derivative f'^{-1} at f(a).

Русский

В одномерном случае существует локальная обратная g с производной f'^{-1} в точке f(a).

LaTeX

$$$\text{HasStrictDerivAt } f f' a \wedge f' \neq 0 \Rightarrow \exists g, \text{HasStrictDerivAt } g f'^{-1} (f a)$$$

Lean4

/-- A function that is inverse to `f` near `a`. -/
abbrev localInverse : 𝕜 → 𝕜 :=
  (hf.hasStrictFDerivAt_equiv hf').localInverse _ _ _

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