latToBddLatCompDualIsoDualCompLatToBddLat

Mathlib.Order.Category.BddLat

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

Lean4

/-- `latToBddLat` and `OrderDual` commute. -/
def latToBddLatCompDualIsoDualCompLatToBddLat : latToBddLat.{u} ⋙ BddLat.dual ≅ Lat.dual ⋙ latToBddLat :=
  Adjunction.leftAdjointUniq (latToBddLatForgetAdjunction.comp BddLat.dualEquiv.toAdjunction)
    (Lat.dualEquiv.toAdjunction.comp latToBddLatForgetAdjunction)

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

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

Разделы

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

Аффилиация

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