implicitToOpenPartialHomeomorph_self

English

There is a globally defined implicit function mapping a pair (z,y) ∈ F × ker f' to a point in E such that f at that point equals z, aligning with the complemented derivative data.

Русский

Существует глобальная неявная функция, которая для пары (z, y) ∈ F × ker f' задаёт точку в E, для которой значение f равно z, согласуясь с данными дополненного производного.

LaTeX

$$$ hf.implicitFunction(f,f',hf',hker) : F × ker f' \to E \text{ с } f( hf.implicitFunction(f,f',hf',hker)(z,y) ) = z$$$

Lean4

@[simp]
theorem implicitToOpenPartialHomeomorph_self (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    hf.implicitToOpenPartialHomeomorph f f' hf' a = (f a, 0) :=
  haveI := FiniteDimensional.complete 𝕜 F
  implicitToOpenPartialHomeomorphOfComplemented_self ..

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