implicitFunctionOfComplemented_apply_image

English

The implicit function of complemented derivatives correctly inverts f on the image: applying the complemented implicit function to the pair (f a, 0) yields a.

Русский

Неявная функция в дополненном виде восстанавливает исходное: применение неявной функции к паре (f(a), 0) даёт a.

LaTeX

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

Lean4

@[simp]
theorem implicitFunctionOfComplemented_apply_image (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
    (hker : (ker f').ClosedComplemented) : hf.implicitFunctionOfComplemented f f' hf' hker (f a) 0 = a := by
  simpa only [implicitToOpenPartialHomeomorphOfComplemented_self] using
    (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).left_inv
      (hf.mem_implicitToOpenPartialHomeomorphOfComplemented_source hf' hker)

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