eventually_right_inverse — Mathlib

English

There exists a neighborhood of f(a) such that composing f with the local inverse yields the identity on that neighborhood.

Русский

Существует окрестность точки f(a), в которой композиция f с локальным обратным даёт тождество.

LaTeX

$$$ \exists V \in 𝓝(f(a)), \forall y \in V, f(hf.localInverse f f' a (y)) = y $$$

Lean4

theorem eventually_right_inverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ y in 𝓝 (f a), f (hf.localInverse f f' a y) = y :=
  (hf.toOpenPartialHomeomorph f).eventually_right_inverse' hf.mem_toOpenPartialHomeomorph_source

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