localInverse_continuousAt — Mathlib

English

The local inverse tends to a as its input tends to f(a).

Русский

Локальное обратное стремится к a, когда входной аргумент стремится к f(a).

LaTeX

$$$ \mathrm{Tendsto} (hf.localInverse f f' a) (\mathcal{N}(f a)) (\mathcal{N}(a)) $$$

Lean4

theorem localInverse_continuousAt (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ContinuousAt (hf.localInverse f f' a) (f a) :=
  (hf.toOpenPartialHomeomorph f).continuousAt_symm hf.image_mem_toOpenPartialHomeomorph_target

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