English
There is a globally defined implicit function that serves as a right inverse on its domain, mapping back to a in E when applied to (f(a), 0).
Русский
Существует глобальная неявная функция, которая служит правой обратной на своей области, возвращая a из E при применении к (f(a), 0).
LaTeX
$$$ hf.implicitFunction f f' hf' hker (f(a),0) = a$$$
Lean4
theorem tendsto_implicitFunction (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) {α : Type*} {l : Filter α}
{g₁ : α → F} {g₂ : α → ker f'} (h₁ : Tendsto g₁ l (𝓝 <| f a)) (h₂ : Tendsto g₂ l (𝓝 0)) :
Tendsto (fun t => hf.implicitFunction f f' hf' (g₁ t) (g₂ t)) l (𝓝 a) :=
by
refine
((hf.implicitToOpenPartialHomeomorph f f' hf').tendsto_symm
(hf.mem_implicitToOpenPartialHomeomorph_source hf')).comp
?_
rw [implicitToOpenPartialHomeomorph_self]
exact h₁.prodMk_nhds h₂
