implicitToOpenPartialHomeomorph_apply_ker

English

There exists a local inverse around a that maps (f(a),0) back to a, provided the hypotheses hold (surjectivity of f' and complemented ker).

Русский

При соблюдении условий существования обратной функции локально около a имеется локальная обратная функция, отправляющая (f(a),0) обратно в a.

LaTeX

$$$\exists \text{local inverse } g: (F \times \ker f') \dashrightarrow E \text{ near } (f(a),0) \text{ s.t. } f(g(z,y)) = z$ near (f(a),0)$$

Lean4

@[simp]
theorem implicitToOpenPartialHomeomorph_apply_ker (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) (y : ker f') :
    hf.implicitToOpenPartialHomeomorph f f' hf' (y + a) = (f (y + a), y) :=
  haveI := FiniteDimensional.complete 𝕜 F
  implicitToOpenPartialHomeomorphOfComplemented_apply_ker ..

Похожие утверждения