English
There is a natural construction producing an open partial homeomorphism between E and F × ker f', under the assumption that f' is surjective and ker f' is complemented.
Русский
Существует естественное построение открытого частичного гомоморфа между E и F × ker f' при условии сюръективности f' и дополненности ker f'.
LaTeX
$$$\text{implicitToOpenPartialHomeomorph}(hf, hf') : OpenPartialHomeomorph\ E\ (F \times \ker f')$$$
Lean4
/-- Given a map `f : E → F` to a finite-dimensional space with a surjective derivative `f'`,
returns an open partial homeomorphism between `E` and `F × ker f'`. -/
def implicitToOpenPartialHomeomorph (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
OpenPartialHomeomorph E (F × ker f') :=
haveI := FiniteDimensional.complete 𝕜 F
hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' f'.ker_closedComplemented_of_finiteDimensional_range
