toOpenPartialHomeomorph_coe — Mathlib

English

If a function f has a strict derivative at a, represented by an invertible continuous linear map f', then the forward component of the local open partial homeomorph attached to f coincides with f itself.

Русский

Если функция f имеет строгую производную в точке a, представленную обратимой непрерывной линейной картой f', то передовая часть локального открытого частичного гомоморфизма, связанная с f, совпадает с самой функцией f.

LaTeX

$$$ (hf.toOpenPartialHomeomorph f) = f $$$

Lean4

@[simp]
theorem toOpenPartialHomeomorph_coe (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    (hf.toOpenPartialHomeomorph f : E → F) = f :=
  rfl

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