localInverse — Mathlib

English

The local inverse is defined as the inverse of the local open partial homeomorph attached to f.

Русский

Локальный обратный задаётся как обратное локального открытого частичного гомоморфизма, связанного с f.

LaTeX

$$$ \operatorname{localInverse} (hf) = (hf.toOpenPartialHomeomorph f)^{-1} $$$

Lean4

/-- Given a function `f` with an invertible derivative, returns a function that is locally inverse
to `f`. -/
def localInverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : F → E :=
  (hf.toOpenPartialHomeomorph f).symm

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