Structures · Order
CompleteBooleanAlgebra
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
- Shape
- One type argument · adds le_sup_inf, inf_compl_le_bot, top_le_sup_compl, sdiff_eq, himp_eq
Extends2
Extended by1
Forgetful instances
Every CompleteBooleanAlgebra is also a
Concrete types that are instances6
- Bool
- SetSemiring
- CategoryTheory.MorphismProperty
- Prod
- OrderDual
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by44
- compl_iInf
- compl_iSup
- CompleteBooleanAlgebra.toCompl
- iSup_symmDiff_le
- iSup_symmDiff_iSup_le
- sSup_symmDiff_le
- iSup_disjointed
- symmDiff_sSup_le
- Filter.limsup_compl
- sSup_symmDiff_sSup_le
- BooleanSubalgebra.iInf_mem
- biSup_symmDiff_biSup_le
- compl_sInf
- Filter.liminf_compl
- disjointed_eq_inf_compl
- BooleanSubalgebra.iSup_mem
- BooleanSubalgebra.sInf_mem
- CompleteBooleanAlgebra.toHImp
- compl_sSup
- BooleanSubalgebra.sSup_mem
- BooleanSubalgebra.biSup_mem
- BooleanSubalgebra.biInf_mem
- CompleteBooleanAlgebra.toSDiff
- symmDiff_iSup_le
- Function.Injective.completeBooleanAlgebra
- Prod.instCompleteBooleanAlgebra
- Equiv.completeBooleanAlgebra
- Filter.sdiff_limsup
- CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra
- Filter.liminf_sdiff
- CompleteBooleanAlgebra.le_sup_inf
- Pi.instCompleteBooleanAlgebra
- CompleteBooleanAlgebra.top_le_sup_compl
- CompleteBooleanAlgebra.sdiff_eq
- OrderDual.instCompleteBooleanAlgebra
- CompleteBooleanAlgebra.toCompleteLattice
- compl_sInf'
- compl_sSup'
- CompleteBooleanAlgebra.inf_compl_le_bot
- CompleteBooleanAlgebra.himp_eq
- Filter.limsup_sdiff
- CompleteBooleanAlgebra.toCompleteDistribLattice
- Filter.sdiff_liminf
- CompleteBooleanAlgebra.toBooleanAlgebra
Ancestors46
- BiheytingAlgebra
- BooleanAlgebra
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- CoheytingAlgebra
- Compl
- CompleteDistribLattice
- CompleteLattice
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- ConditionallyCompleteLattice
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- DistribLattice
- GeneralizedBooleanAlgebra
- GeneralizedCoheytingAlgebra
- GeneralizedHeytingAlgebra
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HImp
- HNot
- HeytingAlgebra
- InfSet
- LE
- LT
- Lattice
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- Order.Coframe
- Order.Frame
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SDiff
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top