toOpenPartialHomeomorph

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#Topology.IsOpenEmbedding.toOpenPartialHomeomorph

Lean4

/-- An open embedding of `X` into `Y`, with `X` nonempty, defines an open partial homeomorphism
whose source is all of `X`. The converse is also true; see
`OpenPartialHomeomorph.to_isOpenEmbedding`. -/
@[simps! (attr := mfld_simps) -fullyApplied apply source target]
noncomputable def toOpenPartialHomeomorph [Nonempty X] : OpenPartialHomeomorph X Y :=
  OpenPartialHomeomorph.ofContinuousOpen (h.isEmbedding.injective.injOn.toPartialEquiv f univ) h.continuous.continuousOn
    h.isOpenMap isOpen_univ

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

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

Разделы

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

Аффилиация

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