instBooleanAlgebra

Mathlib.Order.Booleanisation

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

Lean4

instance instBooleanAlgebra : BooleanAlgebra (Booleanisation α)
    where
  le_top _ := le_top
  bot_le _ := bot_le
  inf_compl_le_bot
    | lift a => by simp
    | comp a => by simp
  top_le_sup_compl
    | lift a => by simp
    | comp a => by simp
  sdiff_eq
    | lift a, lift b => by simp
    | lift a, comp b => by simp
    | comp a, lift b => by simp
    | comp a, comp b => by simp

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

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

Разделы

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

Аффилиация

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