English
Under the same hypotheses, the implicit function produces a mapping that serves as a right inverse to f on inputs of the form (z, y) with z ∈ F and y ∈ ker f'. In particular, for such pairs sufficiently close to (f(a), 0), f evaluated at the implicit image returns z.
Русский
При тех же предположениях имплицитная функция образует отображение, которое является правой обратной к f на аргументах вида (z, y) с z ∈ F и y ∈ ker f'. При этом для пар, близких к (f(a), 0), значение f на полученном изображении равно z.
LaTeX
$$$\forall p \,\in \, F \times \ker f',\ f\bigl(\text{hf.implicitFunctionOfComplemented}(f,f',hf',hker)\,p_1\,p_2\bigr) = p_1.$$$
Lean4
/-- `HasStrictFDerivAt.implicitFunctionOfComplemented` sends `(z, y)` to a point in `f ⁻¹' z`. -/
theorem map_implicitFunctionOfComplemented_eq (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
(hker : (ker f').ClosedComplemented) :
∀ᶠ p : F × ker f' in 𝓝 (f a, 0), f (hf.implicitFunctionOfComplemented f f' hf' hker p.1 p.2) = p.1 :=
((hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).eventually_right_inverse <|
hf.mem_implicitToOpenPartialHomeomorphOfComplemented_target hf' hker).mono
fun ⟨_, _⟩ h => congr_arg Prod.fst h
