English
Let f: E → F have a strict derivative f' at a, with surjective derivative and a kernel that is complemented. Then the canonical open partial homeomorphism between E and F × ker f' obtained from the implicit function theorem places the point (f(a), 0) inside its target, i.e., (f(a), 0) is realized as the image of a nearby point in E under the implicit parametrization.
Русский
Пусть f: E → F имеет строгую производную f' в точке a, производная перезапускаемая на всю F (range f' = ⊤) и ker f' дополнена. Тогда соответствующее открытому частичному гомоморфизму отображение между E и F × ker f' порождается неявной теоремой о функции, и точка (f(a), 0) принадлежит её цели, то есть существует точка близко к a, которая соответствует этому паре.
LaTeX
$$$ (f(a),0) \in (\text{implicitToOpenPartialHomeomorphOfComplemented}(f,f',hf',hker)).target $$$
Lean4
theorem mem_implicitToOpenPartialHomeomorphOfComplemented_target (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
(hker : (ker f').ClosedComplemented) :
(f a, (0 : ker f')) ∈ (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).target := by
simpa only [implicitToOpenPartialHomeomorphOfComplemented_self] using
(hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).map_source <|
hf.mem_implicitToOpenPartialHomeomorphOfComplemented_source hf' hker
