mathlib documentation

• compl : α → α

Set / lattice complement

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
• le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• compl : α → α
• sdiff : α → α → α
• inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ
• sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ

A boolean algebra is a bounded distributive lattice with a complementation operation - such that x ⊓ - x = ⊥ and x ⊔ - x = ⊤. This is a generalization of (classical) logic of propositions, or the powerset lattice.