English
There exists a neighborhood of a such that the implicit representation provided by the complemented implicit function agrees with the original point: for all x nearby a, the point obtained by applying the implicit function to (f x, the corresponding ker-component) returns x.
Русский
Существует окрестность точки a, в которой неявное представление, заданное дополненной функцией, совпадает с исходной точкой: для всех ближайших x к a, точка, полученная применением имплицитной функции к (f(x), соответствующему компоненту в ker f'), возвращает x.
LaTeX
$$$\forall x\text{ near }a,\ hf.implicitFunctionOfComplemented(f,f',hf',hker)(f(x),\; (hf.implicitToOpenPartialHomeomorphOfComplemented(f,f',hf',hker)\,x).snd) = x$$$
Lean4
/-- Any point in some neighborhood of `a` can be represented as
`HasStrictFDerivAt.implicitFunctionOfComplemented` of some point. -/
theorem eq_implicitFunctionOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
(hker : (ker f').ClosedComplemented) :
∀ᶠ x in 𝓝 a,
hf.implicitFunctionOfComplemented f f' hf' hker (f x)
(hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker x).snd =
x :=
(implicitFunctionDataOfComplemented f f' hf hf' hker).implicitFunction_apply_image
