localInverse_tendsto — Mathlib

English

If a function g satisfies g(f x) = x near a, then g agrees with the local inverse on a neighborhood of f(a).

Русский

Если g удовлетворяет g(f x) = x близко к a, тогда g совпадает с локальным обратным на окрестности f(a).

LaTeX

$$$ \forall^\infty y \in 𝓝(f a),\; g(y) = \operatorname{localInverse} f f' a hf y $$$

Lean4

theorem localInverse_tendsto (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    Tendsto (hf.localInverse f f' a) (𝓝 <| f a) (𝓝 a) :=
  (hf.toOpenPartialHomeomorph f).tendsto_symm hf.mem_toOpenPartialHomeomorph_source

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