mem_implicitToOpenPartialHomeomorphOfComplemented_source

English

The base point a belongs to the source of the open partial homeomorph associated to the complemented derivative.

Русский

Базовая точка a принадлежит источнику открытого частичного гомоморфизма, связанного с дополненным производным.

LaTeX

$$a ∈ (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).source$$

Lean4

theorem mem_implicitToOpenPartialHomeomorphOfComplemented_source (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) :
    a ∈ (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).source :=
  ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source _

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