instSup

Mathlib.Order.Booleanisation

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

Lean4

/-- The supremum on `Booleanisation α` is as follows: For `a b : α`,
* `a ⊔ b` is `a ⊔ b`
* `a ⊔ bᶜ` is `(b \ a)ᶜ`
* `aᶜ ⊔ b` is `(a \ b)ᶜ`
* `aᶜ ⊔ bᶜ` is `(a ⊓ b)ᶜ` -/
instance instSup : Max (Booleanisation α) where
  max
    | lift a, lift b => lift (a ⊔ b)
    | lift a, comp b => comp (b \ a)
    | comp a, lift b => comp (a \ b)
    | comp a, comp b => comp (a ⊓ b)

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

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

Разделы

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

Аффилиация

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