English
If f has a strict derivative at a with inverse f' and g is a local right-inverse of f near a, then g agrees with the canonical local inverse on a neighborhood of f(a).
Русский
Если у f есть строгий производный в точке a и обратная часть f' существующих локально, и g является локальным правым инверсом f около a, то g совпадает с каноническим локальным обратным на окрестности f(a).
LaTeX
$$$hf: HasStrictFDerivAt\ f\ f'\ a \land hg: g\text{ является локальным правым обратным }(f) \Rightarrow \forall y\ near(f(a)),\ g(y)=localInverse f f' a hf(y).$$$
Lean4
theorem localInverse_unique (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) {g : F → E} (hg : ∀ᶠ x in 𝓝 a, g (f x) = x) :
∀ᶠ y in 𝓝 (f a), g y = localInverse f f' a hf y :=
eventuallyEq_of_left_inv_of_right_inv hg hf.eventually_right_inverse <|
(hf.toOpenPartialHomeomorph f).tendsto_symm hf.mem_toOpenPartialHomeomorph_source
