Structures · Order

BooleanAlgebra

A Boolean algebra is a bounded distributive lattice with a complement operator ᶜ such that x ⊓ xᶜ = ⊥ and x ⊔ xᶜ = ⊤. For convenience, it must also provide a set difference operation \ and a Heyting implication ⇨ satisfying x \ y = x ⊓ yᶜ and x ⇨ y = y ⊔ xᶜ. This is a generalization of (classical) logic of propositions, or the powerset lattice. Since BoundedOrder, OrderBot, and OrderTop are mixins that require LE to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying Bot and Top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to BoundedOrder is provided.

Defined in

Mathlib.Order.BooleanAlgebra.Defs

Shape

One type argument · adds inf_compl_le_bot, top_le_sup_compl, le_top, bot_le, sdiff_eq, himp_eq