mem_implicitToOpenPartialHomeomorph_source

English

There exists an open partial homeomorphism between E and F × ker f' arising from the derivative data, providing a local parametrization of E by (z, y).

Русский

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

LaTeX

$$$\text{implicitToOpenPartialHomeomorph}(hf, hf') : OpenPartialHomeomorph\ E\ (F \times \ker f')$$$

Lean4

theorem mem_implicitToOpenPartialHomeomorph_source (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    a ∈ (hf.implicitToOpenPartialHomeomorph f f' hf').source :=
  haveI := FiniteDimensional.complete 𝕜 F
  ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source _

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