instInf

Mathlib.Order.Booleanisation

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

Lean4

/-- The infimum on `Booleanisation α` is as follows: For `a b : α`,
* `a ⊓ b` is `a ⊓ b`
* `a ⊓ bᶜ` is `a \ b`
* `aᶜ ⊓ b` is `b \ a`
* `aᶜ ⊓ bᶜ` is `(a ⊔ b)ᶜ` -/
instance instInf : Min (Booleanisation α) where
  min
    | lift a, lift b => lift (a ⊓ b)
    | lift a, comp b => lift (a \ b)
    | comp a, lift b => lift (b \ a)
    | comp a, comp b => comp (a ⊔ b)

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

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

Разделы

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

Аффилиация

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