Documentation

Mathlib.Data.Set.BooleanAlgebra

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 #

Complete lattice and complete Boolean algebra instances #

instance Set.instOrderTop {α : Type u_1} :
Equations