implicitToOpenPartialHomeomorphOfComplemented_self

English

Evaluating the open partial homeomorphism at the base point a yields (f(a), 0).

Русский

При обращении к открытому частичному гомоморфизму в точке a получаем (f(a), 0).

LaTeX

$$hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker a = (f a, 0)$$

Lean4

@[simp]
theorem implicitToOpenPartialHomeomorphOfComplemented_self (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) :
    hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker a = (f a, 0) := by
  simp [hf.implicitToOpenPartialHomeomorphOfComplemented_apply]

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