Sets are a complete atomic boolean algebra. #
This file contains only the definition of the complete atomic boolean algebra structure on Set
.
Indexed union/intersection are defined in Mathlib.Order.SetNotation
; lemmas are available in
Mathlib.Data.Set.Lattice
.
Main declarations #
Set.completeAtomicBooleanAlgebra
:Set α
is aCompleteAtomicBooleanAlgebra
with≤ = ⊆
,< = ⊂
,⊓ = ∩
,⊔ = ∪
,⨅ = ⋂
,⨆ = ⋃
and\
as the set difference. SeeSet.instBooleanAlgebra
.