English
There is a canonical equivalence between E and F × ker f' on an open set, encapsulated by the complemented implicit open partial homeomorph.
Русский
Существует каноническое эквивалентное отображение между E и F × ker f' на открытой области, зашодженной дополненной неявной открытой частичной гомоморфией.
LaTeX
$$$\text{implicitToOpenPartialHomeomorph}(hf, hf') : OpenPartialHomeomorph E (F \times \ker f')$$$
Lean4
/-- Any point in some neighborhood of `a` can be represented as `HasStrictFDerivAt.implicitFunction`
of some point. -/
theorem eq_implicitFunction (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
∀ᶠ x in 𝓝 a, hf.implicitFunction f f' hf' (f x) (hf.implicitToOpenPartialHomeomorph f f' hf' x).snd = x :=
haveI := FiniteDimensional.complete 𝕜 F
eq_implicitFunctionOfComplemented ..
