Theorems · Inductive type · order theory
CompleteBooleanAlgebra
Type u_1 → Type u_1
A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice. It is only completely distributive if it is also atomic.
- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 0 from the axioms · 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 by52
Results whose statement or proof uses this declaration.
- compl_iInfstatement and proof · cited by 6
- compl_iSupstatement and proof · cited by 6
- CompleteBooleanAlgebra.toComplstatement and proof · cited by 4
- iSup_symmDiff_iSup_lestatement and proof · cited by 3
- iSup_symmDiff_lestatement and proof · cited by 3
- sSup_symmDiff_lestatement and proof · cited by 3
- symmDiff_sSup_lestatement and proof · cited by 2
- iSup_disjointedstatement and proof · cited by 2
- Filter.limsup_complstatement and proof · cited by 2
- symmDiff_iSup_lestatement and proof · cited by 1
- biSup_symmDiff_biSup_lestatement and proof · cited by 1
- compl_sInfstatement and proof · cited by 1