implicitToOpenPartialHomeomorphOfComplemented_apply

English

The implicit function corresponding to a complemented derivative is a map F → ker f' → E giving the solution of f(x) = y.

Русский

Неявная функция, соответствующая дополненному производному, задаёт отображение F → ker f' → E, которое даёт решение f(x) = y.

LaTeX

$$implicitFunctionOfComplemented (f) (f') (hf) (hf') (hker) : F → ker f' → E$$

Lean4

theorem implicitToOpenPartialHomeomorphOfComplemented_apply (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) (y : E) :
    hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker y = (f y, Classical.choose hker (y - a)) :=
  rfl

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