toHomeomorph

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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

Lean4

/-- A function `f` that approximates a linear equivalence on the whole space is a homeomorphism. -/
def toHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) univ c) (hc : Subsingleton E ∨ c < N⁻¹) : E ≃ₜ F :=
  by
  refine (hf.toOpenPartialHomeomorph _ _ hc isOpen_univ).toHomeomorphOfSourceEqUnivTargetEqUniv rfl ?_
  rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]
  exact hf.surjective hc

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

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

Разделы

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

Аффилиация

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