mem_implicitToOpenPartialHomeomorph_target

English

The target of the complemented implicit open partial homeomorph contains a neighborhood of (f(a), 0).

Русский

Цель дополненного открытого частичного гомоморфизма содержит окрестность точки (f(a), 0).

LaTeX

$$$ (f(a),0) \in (\text{implicitToOpenPartialHomeomorph}(f,f',hf',hker)).target $$$

Lean4

theorem mem_implicitToOpenPartialHomeomorph_target (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
    (f a, (0 : ker f')) ∈ (hf.implicitToOpenPartialHomeomorph f f' hf').target :=
  haveI := FiniteDimensional.complete 𝕜 F
  mem_implicitToOpenPartialHomeomorphOfComplemented_target ..

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