mk

Mathlib.Topology.Order.Category.AlexDisc

URI: https://scilib.ai/kg/mathlib#AlexDisc.Iso.mk

Lean4

/-- Constructs an equivalence between preorders from an order isomorphism between them. -/
@[simps]
def mk {α β : AlexDisc} (e : α ≃ₜ β) : α ≅ β
    where
  hom := TopCat.ofHom (e : ContinuousMap α β)
  inv := TopCat.ofHom (e.symm : ContinuousMap β α)
  hom_inv_id := by ext; apply e.symm_apply_apply
  inv_hom_id := by ext; apply e.apply_symm_apply

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

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

Разделы

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

Аффилиация

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