LT

Mathlib.Order.Booleanisation

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

Lean4

/-- The order on `Booleanisation α` is as follows: For `a b : α`,
* `a < b` iff `a < b` in `α`
* `a < bᶜ` iff `a` and `b` are disjoint in `α`
* `aᶜ < bᶜ` iff `b < a` in `α`
* `¬ aᶜ < b` -/
protected inductive LT : Booleanisation α → Booleanisation α → Prop
  | protected lift {a b} : a < b → Booleanisation.LT (lift a) (lift b)
  | protected comp {a b} : a < b → Booleanisation.LT (comp b) (comp a)
  | protected sep {a b} : Disjoint a b → Booleanisation.LT (lift a) (comp b)

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

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

Разделы

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

Аффилиация

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