English
The map from E to F × ker f' sending a to the pair (f(a), the ker-component of a) is compatible with the implicit function: applying the implicit function to (f(a), the corresponding ker-component) returns a.
Русский
Отображение из E в F × ker f', отправляющее a ↦ (f(a), компонент ядра), согласуется с неявной функцией: применение неявной функции к (f(a), соответствующей компоненте ker f') возвращает a.
LaTeX
$$$ hf.implicitToOpenPartialHomeomorph(f,f',hf') \, a = (f(a), (hf.implicitToOpenPartialHomeomorphOfComplemented(f,f',hf',hker)\, a).snd)$$$
Lean4
/-- Implicit function `g` defined by `f (g z y) = z`. -/
def implicitFunction (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) : F → ker f' → E :=
Function.curry <| (hf.implicitToOpenPartialHomeomorph f f' hf').symm
