Structures · Order

CompleteAtomicBooleanAlgebra

A complete atomic Boolean algebra is a complete Boolean algebra that is also completely distributive. We take iSup_iInf_eq as the definition here, and prove later on that this implies atomicity.

Defined in: Mathlib.Order.CompleteBooleanAlgebra
Shape: One type argument · adds iInf_iSup_eq

Open in Mathlib docs

Extends1

CompleteBooleanAlgebra

Extended by0

Nothing extends this class yet.

Forgetful instances

Every CompleteAtomicBooleanAlgebra is also a

CompletelyDistribLattice

Concrete types that are instances8

Bool
Language
SimpleGraph
Digraph
Prod
OrderDual
PUnit
Set

How is a type an instance?

Loading the hierarchy index…

Assumed by13

CompleteAtomicBooleanAlgebra.eq_setOfPred_le_sSup_and_isAtom
CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice
CompleteAtomicBooleanAlgebra.instIsAtomistic
Pi.instCompleteAtomicBooleanAlgebra
CompleteAtomicBooleanAlgebra.toSetOfIsAtom
CompleteAtomicBooleanAlgebra.iInf_iSup_eq
CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom
Equiv.completeAtomicBooleanAlgebra
Function.Injective.completeAtomicBooleanAlgebra
CompleteAtomicBooleanAlgebra.instIsCoatomistic
CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra
Prod.instCompleteAtomicBooleanAlgebra
OrderDual.instCompleteAtomicBooleanAlgebra