English
Let E, F, G be normed spaces over a nontrivial normed field 𝕜, and let f: E → F and g: E → G be maps that are strictly differentiable at a and whose derivatives are surjective with complementary kernels. Then the map x ↦ (f x, g x) defines an open partial homeomorphism between E and F × G; in particular, the level set {x ∈ E : f x = f a} is locally homeomorphic to G.
Русский
Пусть E, F, G — нормированные пространства над ненулевым нормированным полем 𝕜, а функции f: E → F и g: E → G строго дифференцируемы в точке a; их производные сюрьективны и их ядра дополнены. Тогда отображение x ↦ (f x, g x) задаёт открытое частичное гомеоморфизм между E и F × G; в частности, множество {x ∈ E : f x = f a} локально гомеоморфно к G.
LaTeX
$$$$\text{Let } E, F, G \text{ be normed spaces over } 𝕜,\; f:E\to F, \; g:E\to G. \text{ Suppose } f'=:Df(a) \text{ and } g':=Dg(a) \text{ are surjective and } \ker f' \oplus \ker g' = E. \text{ Then } x \mapsto (f(x),g(x)) \text{ induces an open partial homeomorphism } E \dashrightarrow F \times G.$$$$
Lean4
/-- Implicit function theorem. If `f : E → F` and `g : E → G` are two maps strictly differentiable
at `a`, their derivatives `f'`, `g'` are surjective, and the kernels of these derivatives are
complementary subspaces of `E`, then `x ↦ (f x, g x)` defines an open partial homeomorphism between
`E` and `F × G`. In particular, `{x | f x = f a}` is locally homeomorphic to `G`. -/
def toOpenPartialHomeomorph : OpenPartialHomeomorph E (F × G) :=
φ.hasStrictFDerivAt.toOpenPartialHomeomorph _
