LE

Mathlib.Order.Booleanisation

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

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 LE : Booleanisation α → Booleanisation α → Prop
  | protected lift {a b} : a ≤ b → Booleanisation.LE (lift a) (lift b)
  | protected comp {a b} : a ≤ b → Booleanisation.LE (comp b) (comp a)
  | protected sep {a b} : Disjoint a b → Booleanisation.LE (lift a) (comp b)

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

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

Разделы

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

Аффилиация

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