instPartialOrder

Mathlib.Order.Booleanisation

URI: https://scilib.ai/kg/mathlib#Booleanisation.instPartialOrder

Lean4

instance instPartialOrder : PartialOrder (Booleanisation α) where
  le_antisymm
    | lift a, lift b, LE.lift hab, LE.lift hba => by rw [hab.antisymm hba]
    | comp a, comp b, LE.comp hab, LE.comp hba => by
      rw [hab.antisymm hba]
        -- The linter significantly hinders readability here.

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

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

Разделы

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

Аффилиация

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