# mathlibdocumentation

order.boolean_algebra

# (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 α.

generalized_boolean_algebra α 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 boolean_algebra type class is defined to extend generalized_boolean_algebra 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 #

• has_compl: a type class for the complement operator
• generalized_boolean_algebra: a type class for generalized Boolean algebras
• boolean_algebra.core: a type class with the minimal assumptions for a Boolean algebras
• boolean_algebra: the main type class for Boolean algebras; it extends both generalized_boolean_algebra and boolean_algebra.core. An instance of boolean_algebra can be obtained from one of boolean_algebra.core using boolean_algebra.of_core.
• boolean_algebra_Prop: the Boolean algebra instance on Prop

## Implementation notes #

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

Stone's paper introducing generalized Boolean algebras 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.

## Notations #

• xᶜ is notation for compl x
• x \ y is notation for sdiff x y.

## Tags #

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