alexDiscEquivPreord

Mathlib.Topology.Order.Category.AlexDisc

URI: https://scilib.ai/kg/mathlib#alexDiscEquivPreord

Lean4

/-- Sends a topological space to its specialisation order. -/
@[simps]
def alexDiscEquivPreord : AlexDisc ≌ Preord
    where
  functor := forget₂ _ _ ⋙ topToPreord
  inverse.obj X := AlexDisc.of (WithUpperSet X)
  inverse.map f := TopCat.ofHom (WithUpperSet.map f.hom)
  unitIso := NatIso.ofComponents fun X ↦ AlexDisc.Iso.mk <| by dsimp; exact homeoWithUpperSetTopologyorderIso X
  counitIso :=
    NatIso.ofComponents fun X ↦ Preord.Iso.mk <| by dsimp; exact (orderIsoSpecializationWithUpperSetTopology X).symm

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

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

Разделы

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

Аффилиация

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