Theorems · Inductive type · order theory
BooleanAlgebra
Type u → Type u
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
- Cited by
- 300 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by348
Results whose statement or proof uses this declaration.
- compl_complstatement and proof · cited by 229
- BooleanSubalgebrastatement · cited by 104
- Finset.complsstatement and proof · cited by 34
- compl_surjectivestatement and proof · cited by 26
- compl_injectivestatement and proof · cited by 22
- isCompl_complstatement and proof · cited by 21
- BooleanSubalgebra.mapstatement and proof · cited by 20
- sdiff_eqstatement and proof · cited by 18
- compl_inj_iffstatement and proof · cited by 15
- BoolAlg.ofHomstatement and proof · cited by 14
- BooleanSubalgebra.comapstatement and proof · cited by 14
- compl_infstatement and proof · cited by 12
Showing the 200 most cited of 348.