# Documentation

Mathlib.Order.BooleanAlgebra

# (Generalized) Boolean algebras #

A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras generalize the (classical) logic of propositions and the lattice of subsets of a set.

Generalized Boolean algebras may be less familiar, but they are essentially Boolean algebras which do not necessarily have a top element (⊤⊤) (and hence not all elements may have complements). One example in mathlib is Finset α, the type of all finite subsets of an arbitrary (not-necessarily-finite) type α.

GeneralizedBooleanAlgebra α is defined to be a distributive lattice with bottom (⊥⊥) admitting a relative complement operator, written using "set difference" notation as x \ y (sdiff x y). For convenience, the BooleanAlgebra type class is defined to extend GeneralizedBooleanAlgebra so that it is also bundled with a \ operator.

(A terminological point: x \ y is the complement of y relative to the interval [⊥, x]⊥, x]. We do not yet have relative complements for arbitrary intervals, as we do not even have lattice intervals.)

## Main declarations #

• GeneralizedBooleanAlgebra: a type class for generalized Boolean algebras
• BooleanAlgebra: a type class for Boolean algebras.
• Prop.booleanAlgebra: the Boolean algebra instance on Prop

## Implementation notes #

The sup_inf_sdiff and inf_inf_sdiff axioms for the relative complement operator in GeneralizedBooleanAlgebra are taken from Wikipedia.

[Stone's paper introducing generalized Boolean algebras][Stone1935] does not define a relative complement operator a \ b for all a, b. Instead, the postulates there amount to an assumption that for all a, b : α where a ≤ b≤ b, the equations x ⊔ a = b⊔ a = b and x ⊓ a = ⊥⊓ a = ⊥⊥ have a solution x. disjoint.sdiff_unique proves that this x is in fact b \ a.

## Tags #

generalized Boolean algebras, Boolean algebras, lattices, sdiff, compl

### Generalized Boolean algebras #

Some of the lemmas in this section are from:

class GeneralizedBooleanAlgebra (α : Type u) extends , , :
• For any a, b, (a ⊓ b) ⊔ (a / b) = a⊓ b) ⊔ (a / b) = a⊔ (a / b) = a

sup_inf_sdiff : ∀ (a b : α), a b a \ b = a
• For any a, b, (a ⊓ b) ⊓ (a / b) = ⊥⊓ b) ⊓ (a / b) = ⊥⊓ (a / b) = ⊥⊥

inf_inf_sdiff : ∀ (a b : α), a b a \ b =

A generalized Boolean algebra is a distributive lattice with ⊥⊥ and a relative complement operation \ (called sdiff, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a⊓ b) ⊔ (a \ b) = a⊔ (a \ b) = a and (a ⊓ b) ⊓ (a \ b) = ⊥⊓ b) ⊓ (a \ b) = ⊥⊓ (a \ b) = ⊥⊥, i.e. a \ b is the complement of b in a.

This is a generalization of Boolean algebras which applies to Finset α for arbitrary (not-necessarily-Fintype) α.

Instances
@[simp]
theorem sup_inf_sdiff {α : Type u} [inst : ] (x : α) (y : α) :
x y x \ y = x
@[simp]
theorem inf_inf_sdiff {α : Type u} [inst : ] (x : α) (y : α) :
x y x \ y =
@[simp]
theorem sup_sdiff_inf {α : Type u} [inst : ] (x : α) (y : α) :
x \ y x y = x
@[simp]
theorem inf_sdiff_inf {α : Type u} [inst : ] (x : α) (y : α) :
x \ y (x y) =
instance GeneralizedBooleanAlgebra.toOrderBot {α : Type u} [inst : ] :
Equations
• GeneralizedBooleanAlgebra.toOrderBot = let src := GeneralizedBooleanAlgebra.toBot; OrderBot.mk (_ : ∀ (a : α), a)
theorem disjoint_inf_sdiff {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint (x y) (x \ y)
theorem sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [inst : ] (s : x y z = x) (i : x y z = ) :
x \ y = z
@[simp]
theorem sdiff_inf_sdiff {α : Type u} {x : α} {y : α} [inst : ] :
x \ y y \ x =
theorem disjoint_sdiff_sdiff {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint (x \ y) (y \ x)
@[simp]
theorem inf_sdiff_self_right {α : Type u} {x : α} {y : α} [inst : ] :
x y \ x =
@[simp]
theorem inf_sdiff_self_left {α : Type u} {x : α} {y : α} [inst : ] :
y \ x x =
Equations
• One or more equations did not get rendered due to their size.
theorem disjoint_sdiff_self_left {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint (y \ x) x
theorem disjoint_sdiff_self_right {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint x (y \ x)
theorem le_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
x y \ z x y Disjoint x z
@[simp]
theorem sdiff_eq_left {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = x Disjoint x y
theorem Disjoint.sdiff_eq_of_sup_eq {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hi : Disjoint x z) (hs : x z = y) :
y \ x = z
theorem Disjoint.sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hd : Disjoint x z) (hz : z y) (hs : y x z) :
y \ x = z
theorem disjoint_sdiff_iff_le {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hz : z y) (hx : x y) :
Disjoint z (y \ x) z x
theorem le_iff_disjoint_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hz : z y) (hx : x y) :
z x Disjoint z (y \ x)
theorem inf_sdiff_eq_bot_iff {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hz : z y) (hx : x y) :
z y \ x = z x
theorem le_iff_eq_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hz : z y) (hx : x y) :
x z y = z y \ x
theorem sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
y \ (x z) = y \ x y \ z
theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
y \ x = y \ z y x = y z
theorem sdiff_eq_self_iff_disjoint {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = x Disjoint y x
theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = x Disjoint x y
theorem sdiff_lt {α : Type u} {x : α} {y : α} [inst : ] (hx : y x) (hy : y ) :
x \ y < x
@[simp]
theorem le_sdiff_iff {α : Type u} {x : α} {y : α} [inst : ] :
x y \ x x =
theorem sdiff_lt_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : ] (h : x < y) (hz : z x) :
x \ z < y \ z
theorem sup_inf_inf_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
x y z y \ z = x y y \ z
theorem sdiff_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
x \ (y \ z) = x \ y x y z
theorem sdiff_sdiff_right' {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
x \ (y \ z) = x \ y x z
theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [inst : ] (h : z x) :
x \ (y \ z) = x \ y z
@[simp]
theorem sdiff_sdiff_right_self {α : Type u} {x : α} {y : α} [inst : ] :
x \ (x \ y) = x y
theorem sdiff_sdiff_eq_self {α : Type u} {x : α} {y : α} [inst : ] (h : y x) :
x \ (x \ y) = y
theorem sdiff_eq_symm {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hy : y x) (h : x \ y = z) :
x \ z = y
theorem sdiff_eq_comm {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hy : y x) (hz : z x) :
x \ y = z x \ z = y
theorem eq_of_sdiff_eq_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] (hxz : x z) (hyz : y z) (h : z \ x = z \ y) :
x = y
theorem sdiff_sdiff_left' {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
(x \ y) \ z = x \ y x \ z
theorem sdiff_sdiff_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
z \ (x \ y y \ x) = z (z \ x y) (z \ y x)
theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
z \ (x \ y y \ x) = z x y z \ x z \ y
theorem inf_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
(x y) \ z = x \ z y \ z
theorem inf_sdiff_assoc {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
(x y) \ z = x y \ z
theorem inf_sdiff_right_comm {α : Type u} {x : α} {y : α} {z : α} [inst : ] :
x \ z y = (x y) \ z
theorem inf_sdiff_distrib_left {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a b \ c = (a b) \ (a c)
theorem inf_sdiff_distrib_right {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a \ b c = (a c) \ (b c)
theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x : α} {y : α} [inst : ] :
x y = x \ y y \ x x y
theorem sup_lt_of_lt_sdiff_left {α : Type u} {x : α} {y : α} {z : α} [inst : ] (h : y < z \ x) (hxz : x z) :
x y < z
theorem sup_lt_of_lt_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : ] (h : x < z \ y) (hyz : y z) :
x y < z
instance Pi.generalizedBooleanAlgebra {α : Type u} {β : Type v} [inst : ] :
Equations

### Boolean algebras #

class BooleanAlgebra (α : Type u) extends , , , , , :
• The infimum of x and xᶜ is at most ⊥⊥

inf_compl_le_bot : ∀ (x : α), x x
• The supremum of x and xᶜ is at least ⊤⊤

top_le_sup_compl : ∀ (x : α), x x
• ⊤⊤ is the greatest element

le_top : ∀ (a : α), a
• ⊥⊥ is the least element

bot_le : ∀ (a : α), a
• x \ y is equal to x ⊓ yᶜ⊓ yᶜ

sdiff_eq : autoParam (∀ (x y : α), x \ y = x y) _auto✝
• x ⇨ y⇨ y is equal to y ⊔ xᶜ⊔ xᶜ

himp_eq : autoParam (∀ (x y : α), x y = y x) _auto✝

A Boolean algebra is a bounded distributive lattice with a complement operator ᶜ such that x ⊓ xᶜ = ⊥⊓ xᶜ = ⊥⊥ and x ⊔ xᶜ = ⊤⊔ xᶜ = ⊤⊤. For convenience, it must also provide a set difference operation \ and a Heyting implication ⇨⇨ satisfying x \ y = x ⊓ yᶜ⊓ yᶜ and x ⇨ y = y ⊔ xᶜ⇨ y = y ⊔ xᶜ⊔ xᶜ.

This is a generalization of (classical) logic of propositions, or the powerset lattice.

Since BoundedOrder, OrderBot, and OrderTop are mixins that require LE to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying Bot and Top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to BoundedOrder is provided.

Instances
instance BooleanAlgebra.toBoundedOrder {α : Type u} [h : ] :
Equations
• BooleanAlgebra.toBoundedOrder = BoundedOrder.mk
def GeneralizedBooleanAlgebra.toBooleanAlgebra {α : Type u} [inst : ] [inst : ] :

A bounded generalized boolean algebra is a boolean algebra.

Equations
• One or more equations did not get rendered due to their size.
theorem inf_compl_eq_bot' {α : Type u} {x : α} [inst : ] :
@[simp]
theorem sup_compl_eq_top {α : Type u} {x : α} [inst : ] :
@[simp]
theorem compl_sup_eq_top {α : Type u} {x : α} [inst : ] :
theorem isCompl_compl {α : Type u} {x : α} [inst : ] :
theorem sdiff_eq {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = x y
theorem himp_eq {α : Type u} {x : α} {y : α} [inst : ] :
x y = y x
instance BooleanAlgebra.toComplementedLattice {α : Type u} [inst : ] :
Equations
instance BooleanAlgebra.toGeneralizedBooleanAlgebra {α : Type u} [inst : ] :
Equations
instance BooleanAlgebra.toBiheytingAlgebra {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem hnot_eq_compl {α : Type u} {x : α} [inst : ] :
theorem top_sdiff {α : Type u} {x : α} [inst : ] :
\ x = x
theorem eq_compl_iff_isCompl {α : Type u} {x : α} {y : α} [inst : ] :
x = y IsCompl x y
theorem compl_eq_iff_isCompl {α : Type u} {x : α} {y : α} [inst : ] :
x = y IsCompl x y
theorem compl_eq_comm {α : Type u} {x : α} {y : α} [inst : ] :
x = y y = x
theorem eq_compl_comm {α : Type u} {x : α} {y : α} [inst : ] :
x = y y = x
@[simp]
theorem compl_compl {α : Type u} [inst : ] (x : α) :
theorem compl_comp_compl {α : Type u} [inst : ] :
compl compl = id
@[simp]
theorem compl_involutive {α : Type u} [inst : ] :
theorem compl_bijective {α : Type u} [inst : ] :
theorem compl_surjective {α : Type u} [inst : ] :
theorem compl_injective {α : Type u} [inst : ] :
@[simp]
theorem compl_inj_iff {α : Type u} {x : α} {y : α} [inst : ] :
x = y x = y
theorem IsCompl.compl_eq_iff {α : Type u} {x : α} {y : α} {z : α} [inst : ] (h : IsCompl x y) :
z = y z = x
@[simp]
theorem compl_eq_top {α : Type u} {x : α} [inst : ] :
@[simp]
theorem compl_eq_bot {α : Type u} {x : α} [inst : ] :
@[simp]
theorem compl_inf {α : Type u} {x : α} {y : α} [inst : ] :
(x y) = x y
@[simp]
theorem compl_le_compl_iff_le {α : Type u} {x : α} {y : α} [inst : ] :
y x x y
theorem compl_le_of_compl_le {α : Type u} {x : α} {y : α} [inst : ] (h : y x) :
x y
theorem compl_le_iff_compl_le {α : Type u} {x : α} {y : α} [inst : ] :
x y y x
@[simp]
theorem sdiff_compl {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = x y
instance instBooleanAlgebraOrderDual {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem sup_inf_inf_compl {α : Type u} {x : α} {y : α} [inst : ] :
x y x y = x
@[simp]
theorem compl_sdiff {α : Type u} {x : α} {y : α} [inst : ] :
(x \ y) = x y
@[simp]
theorem compl_himp {α : Type u} {x : α} {y : α} [inst : ] :
(x y) = x \ y
theorem compl_sdiff_compl {α : Type u} {x : α} {y : α} [inst : ] :
x \ y = y \ x
@[simp]
theorem compl_himp_compl {α : Type u} {x : α} {y : α} [inst : ] :
x y = y x
theorem disjoint_compl_left_iff {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint (x) y y x
theorem disjoint_compl_right_iff {α : Type u} {x : α} {y : α} [inst : ] :
Disjoint x (y) x y
Equations
• One or more equations did not get rendered due to their size.
instance Pi.booleanAlgebra {ι : Type u} {α : ιType v} [inst : (i : ι) → BooleanAlgebra (α i)] :
BooleanAlgebra ((i : ι) → α i)
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Bool.sup_eq_bor :
(fun x x_1 => x x_1) = or
@[simp]
theorem Bool.inf_eq_band :
(fun x x_1 => x x_1) = and
@[simp]
theorem Bool.compl_eq_bnot :
compl = not
def Function.Injective.generalizedBooleanAlgebra {α : Type u} {β : Type u_1} [inst : Sup α] [inst : Inf α] [inst : Bot α] [inst : ] [inst : ] (f : αβ) (hf : ) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_bot : f = ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

Pullback a GeneralizedBooleanAlgebra along an injection.

Equations
• One or more equations did not get rendered due to their size.
def Function.Injective.booleanAlgebra {α : Type u} {β : Type u_1} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : Bot α] [inst : ] [inst : ] [inst : ] (f : αβ) (hf : ) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f (a) = f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

Pullback a BooleanAlgebra along an injection.

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