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.lean.

Main declarations

• Set.completeAtomicBooleanAlgebra: Set α is a CompleteAtomicBooleanAlgebra with ≤ = ⊆, < = ⊂, ⊓ = ∩, ⊔ = ∪, ⨅ = ⋂, ⨆ = ⋃ and \ as the set difference. See Set.instBooleanAlgebra.

Complete lattice and complete Boolean algebra instances

instance Set.instCompleteAtomicBooleanAlgebra {α : Type u_1} : CompleteAtomicBooleanAlgebra (Set α)

Equations

• One or more equations did not get rendered due to their size.

instance Set.instOrderTop {α : Type u_1} : OrderTop (Set α)

Equations

• Set.instOrderTop = { top := Set.univ, le_top := ⋯ }