implicitToOpenPartialHomeomorphOfComplemented_apply_ker

English

For any y ∈ E, the open partial homeomorphism evaluates to (f(y), choose(hker)(y − a)).

Русский

Для любого y ∈ E отображение открытого частичного гомоморфизма даёт (f(y), выбрать(hker)(y − a)).

LaTeX

$$hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker y = (f y, Classical.choose hker (y - a))$$

Lean4

@[simp]
theorem implicitToOpenPartialHomeomorphOfComplemented_apply_ker (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) (y : ker f') :
    hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker (y + a) = (f (y + a), y) := by
  simp only [implicitToOpenPartialHomeomorphOfComplemented_apply, add_sub_cancel_right, Classical.choose_spec hker]

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