localInverse_apply_image — Mathlib

English

There exists a neighborhood of a on which the local inverse composed with f acts as the identity.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem localInverse_apply_image (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : hf.localInverse f f' a (f a) = a :=
  hf.eventually_left_inverse.self_of_nhds

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