# Documentation

Mathlib.Order.BooleanAlgebra

# (Generalized) Boolean algebras #

A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras generalize the (classical) logic of propositions and the lattice of subsets of a set.

Generalized Boolean algebras may be less familiar, but they are essentially Boolean algebras which do not necessarily have a top element (⊤) (and hence not all elements may have complements). One example in mathlib is Finset α, the type of all finite subsets of an arbitrary (not-necessarily-finite) type α.

GeneralizedBooleanAlgebra α is defined to be a distributive lattice with bottom (⊥) admitting a relative complement operator, written using "set difference" notation as x \ y (sdiff x y). For convenience, the BooleanAlgebra type class is defined to extend GeneralizedBooleanAlgebra so that it is also bundled with a \ operator.

(A terminological point: x \ y is the complement of y relative to the interval [⊥, x]. We do not yet have relative complements for arbitrary intervals, as we do not even have lattice intervals.)

## Main declarations #

• GeneralizedBooleanAlgebra: a type class for generalized Boolean algebras
• BooleanAlgebra: a type class for Boolean algebras.
• Prop.booleanAlgebra: the Boolean algebra instance on Prop

## Implementation notes #

The sup_inf_sdiff and inf_inf_sdiff axioms for the relative complement operator in GeneralizedBooleanAlgebra are taken from Wikipedia.

[Stone's paper introducing generalized Boolean algebras][Stone1935] does not define a relative complement operator a \ b for all a, b. Instead, the postulates there amount to an assumption that for all a, b : α where a ≤ b, the equations x ⊔ a = b and x ⊓ a = ⊥ have a solution x. Disjoint.sdiff_unique proves that this x is in fact b \ a.

• [Postulates for Boolean Algebras and Generalized Boolean Algebras, M.H. Stone][Stone1935]
• [Lattice Theory: Foundation, George Grätzer][Gratzer2011]

## Tags #

generalized Boolean algebras, Boolean algebras, lattices, sdiff, compl