toPartialEquiv

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

URI: https://scilib.ai/kg/mathlib#ApproximatesLinearOn.toPartialEquiv

Lean4

/-- A map approximating a linear equivalence on a set defines a partial equivalence on this set.
Should not be used outside of this file, because it is superseded by `toOpenPartialHomeomorph`
below.

This is a first step towards the inverse function. -/
def toPartialEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
    PartialEquiv E F :=
  (hf.injOn hc).toPartialEquiv _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru