mathlib documentation

order.boolean_algebra

(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 α.

generalized_boolean_algebra α 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 boolean_algebra type class is defined to extend generalized_boolean_algebra so that it is also bundled with a \ operator.

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

Main declarations #

Implementation notes #

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

Stone's paper introducing generalized Boolean algebras 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, the equations x ⊔ a = b and x ⊓ a = ⊥ have a solution x. disjoint.sdiff_unique proves that this x is in fact b \ a.

Notations #

References #

Tags #

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

Generalized Boolean algebras #

Some of the lemmas in this section are from:

@[class]
structure generalized_boolean_algebra (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • bot : α
  • bot_le : ∀ (a : α), a
  • sdiff : α → α → α
  • sup_inf_sdiff : ∀ (a b : α), a b a \ b = a
  • 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 and (a ⊓ b) ⊓ (a \ b) = 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} [generalized_boolean_algebra α] (x y : α) :
x y x \ y = x
@[simp]
theorem inf_inf_sdiff {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x y (x \ y) =
@[simp]
theorem sup_sdiff_inf {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x \ y x y = x
@[simp]
theorem inf_sdiff_inf {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x \ y (x y) =
theorem disjoint_inf_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (x y) (x \ y)
theorem sdiff_unique {α : Type u} {x y z : α} [generalized_boolean_algebra α] (s : x y z = x) (i : x y z = ) :
x \ y = z
theorem sdiff_symm {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hy : y x) (hz : z x) (H : x \ y = z) :
x \ z = y
theorem sdiff_le {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y x
@[simp]
theorem bot_sdiff {α : Type u} {x : α} [generalized_boolean_algebra α] :
theorem inf_sdiff_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x (x \ y) = x \ y
theorem inf_sdiff_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y x = x \ y
@[simp]
theorem sdiff_self {α : Type u} {x : α} [generalized_boolean_algebra α] :
x \ x =
@[simp]
theorem sup_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x y \ x = x y
@[simp]
theorem sup_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x x = y x
theorem sup_sdiff_symm {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x y \ x = y x \ y
theorem sup_sdiff_of_le {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : x y) :
x y \ x = y
@[simp]
theorem sup_sdiff_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x x \ y = x
theorem sup_sdiff_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y x = x
@[simp]
theorem sdiff_inf_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y (y \ x) =
theorem disjoint_sdiff_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (x \ y) (y \ x)
theorem le_sup_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y x y \ x
theorem le_sdiff_sup {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y y \ x x
@[simp]
theorem inf_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x (y \ x) =
@[simp]
theorem inf_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x x =
theorem disjoint_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (y \ x) x
theorem disjoint_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint x (y \ x)
theorem disjoint.disjoint_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : disjoint x y) :
disjoint (x \ z) y
theorem disjoint.disjoint_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : disjoint x y) :
disjoint x (y \ z)
theorem disjoint.sdiff_eq_of_sup_eq {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hi : disjoint x z) (hs : x z = y) :
y \ x = z
theorem disjoint.sup_sdiff_cancel_left {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
(x y) \ x = y
theorem disjoint.sup_sdiff_cancel_right {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
(x y) \ y = x
theorem disjoint.sdiff_unique {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hd : disjoint x z) (hz : z y) (hs : y x z) :
y \ x = z
theorem disjoint_sdiff_iff_le {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hz : z y) (hx : x y) :
disjoint z (y \ x) z x
theorem le_iff_disjoint_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hz : z y) (hx : x y) :
z x disjoint z (y \ x)
theorem inf_sdiff_eq_bot_iff {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hz : z y) (hx : x y) :
z (y \ x) = z x
theorem le_iff_eq_sup_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hz : z y) (hx : x y) :
x z y = z y \ x
theorem sup_sdiff_cancel' {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hx : x z) (hz : z y) :
z y \ x = y
theorem sdiff_sup {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ (x z) = y \ x (y \ z)
theorem sdiff_inf {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ (x z) = y \ x y \ z
@[simp]
theorem sdiff_inf_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ (x y) = y \ x
@[simp]
theorem sdiff_inf_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ (y x) = y \ x
theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ x = y \ z y x = y z
theorem disjoint.sdiff_eq_left {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
x \ y = x
theorem disjoint.sdiff_eq_right {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
y \ x = y
@[simp]
theorem sdiff_bot {α : Type u} {x : α} [generalized_boolean_algebra α] :
x \ = x
theorem sdiff_eq_self_iff_disjoint {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y = x disjoint y x
theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y = x disjoint x y
theorem sdiff_lt {α : Type u} {x y : α} [generalized_boolean_algebra α] (hx : y x) (hy : y ) :
x \ y < x
theorem sdiff_le_sdiff_self {α : Type u} {w x z : α} [generalized_boolean_algebra α] (h : z x) :
w \ x w \ z
theorem sdiff_le_iff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ x z y x z
theorem sdiff_eq_bot_iff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x = y x
theorem sdiff_le_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y z x \ z y
theorem sdiff_le_self_sdiff {α : Type u} {w x y : α} [generalized_boolean_algebra α] (h : w y) :
w \ x y \ x
theorem sdiff_le_sdiff {α : Type u} {w x y z : α} [generalized_boolean_algebra α] (h₁ : w y) (h₂ : z x) :
w \ x y \ z
theorem sup_inf_inf_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x y z y \ z = x y y \ z
@[simp]
theorem inf_sdiff_sup_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ z (x y) = x \ z
@[simp]
theorem inf_sdiff_sup_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ z (y x) = x \ z
theorem sdiff_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ (y \ z) = x \ y x y z
theorem sdiff_sdiff_right' {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ (y \ z) = x \ y x z
@[simp]
theorem sdiff_sdiff_right_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ (x \ y) = x y
theorem sdiff_sdiff_eq_self {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : y x) :
x \ (x \ y) = y
theorem sdiff_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ (y z)
theorem sdiff_sdiff_left' {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ y (x \ z)
theorem sdiff_sdiff_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ z \ y
@[simp]
theorem sdiff_idem {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y \ y = x \ y
@[simp]
theorem sdiff_sdiff_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y \ x =
theorem sdiff_sdiff_sup_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
z \ (x \ y y \ x) = z (z \ x y) (z \ y x)
theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
z \ (x \ y y \ x) = z x y z \ x (z \ y)
theorem sup_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
(x y) \ z = x \ z y \ z
theorem sup_sdiff_right_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
(x y) \ y = x \ y
theorem sup_sdiff_left_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
(x y) \ x = y \ x
theorem inf_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x y \ z = x \ z (y \ z)
theorem inf_sdiff_assoc {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x y \ z = x (y \ z)
theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x y = x \ y y \ x x y
@[instance]
def pi.generalized_boolean_algebra {α : Type u} {β : Type v} [generalized_boolean_algebra β] :
Equations

Boolean algebras #

@[class]
structure has_compl (α : Type u_1) :
Type u_1
  • compl : α → α

Set / lattice complement

Instances
@[class]
structure boolean_algebra.core (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • bot : α
  • bot_le : ∀ (a : α), a
  • top : α
  • le_top : ∀ (a : α), a
  • compl : α → α
  • inf_compl_le_bot : ∀ (x : α), x x
  • top_le_sup_compl : ∀ (x : α), x x

This class contains the core axioms of a Boolean algebra. The boolean_algebra class extends both this class and generalized_boolean_algebra, see Note [forgetful inheritance].

Instances
@[instance]
@[simp]
theorem inf_compl_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
@[simp]
theorem compl_inf_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
@[simp]
theorem sup_compl_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
@[simp]
theorem compl_sup_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
theorem is_compl_compl {α : Type u} {x : α} [boolean_algebra.core α] :
theorem is_compl.eq_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : is_compl x y) :
x = y
theorem is_compl.compl_eq {α : Type u} {x y : α} [boolean_algebra.core α] (h : is_compl x y) :
x = y
theorem eq_compl_iff_is_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
x = y is_compl x y
theorem compl_eq_iff_is_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
x = y is_compl x y
theorem disjoint_compl_right {α : Type u} {x : α} [boolean_algebra.core α] :
theorem disjoint_compl_left {α : Type u} {x : α} [boolean_algebra.core α] :
theorem compl_unique {α : Type u} {x y : α} [boolean_algebra.core α] (i : x y = ) (s : x y = ) :
x = y
@[simp]
theorem compl_top {α : Type u} [boolean_algebra.core α] :
@[simp]
theorem compl_bot {α : Type u} [boolean_algebra.core α] :
@[simp]
theorem compl_compl {α : Type u} [boolean_algebra.core α] (x : α) :
@[simp]
@[simp]
theorem compl_inj_iff {α : Type u} {x y : α} [boolean_algebra.core α] :
x = y x = y
theorem is_compl.compl_eq_iff {α : Type u} {x y z : α} [boolean_algebra.core α] (h : is_compl x y) :
z = y z = x
@[simp]
theorem compl_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
@[simp]
theorem compl_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
@[simp]
theorem compl_inf {α : Type u} {x y : α} [boolean_algebra.core α] :
(x y) = x y
@[simp]
theorem compl_sup {α : Type u} {x y : α} [boolean_algebra.core α] :
(x y) = x y
theorem compl_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : y x) :
@[simp]
theorem compl_le_compl_iff_le {α : Type u} {x y : α} [boolean_algebra.core α] :
y x x y
theorem le_compl_of_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : y x) :
x y
theorem compl_le_of_compl_le {α : Type u} {x y : α} [boolean_algebra.core α] (h : y x) :
x y
theorem le_compl_iff_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
y x x y
theorem compl_le_iff_compl_le {α : Type u} {x y : α} [boolean_algebra.core α] :
x y y x
@[instance]
def boolean_algebra.to_core (α : Type u) [self : boolean_algebra α] :
@[class]
structure boolean_algebra (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • bot : α
  • bot_le : ∀ (a : α), a
  • sdiff : α → α → α
  • sup_inf_sdiff : ∀ (a b : α), a b a \ b = a
  • inf_inf_sdiff : ∀ (a b : α), a b (a \ b) =
  • top : α
  • le_top : ∀ (a : α), a
  • compl : α → α
  • inf_compl_le_bot : ∀ (x : α), x x
  • top_le_sup_compl : ∀ (x : α), x x
  • sdiff_eq : ∀ (x y : α), x \ y = x y

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

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

Instances

Create a boolean_algebra instance from a boolean_algebra.core instance, defining x \ y to be x ⊓ yᶜ.

For some types, it may be more convenient to create the boolean_algebra instance by hand in order to have a simpler sdiff operation.

Equations
theorem sdiff_eq {α : Type u} {x y : α} [boolean_algebra α] :
x \ y = x y
theorem sdiff_compl {α : Type u} {x y : α} [boolean_algebra α] :
x \ y = x y
theorem top_sdiff {α : Type u} {x : α} [boolean_algebra α] :
\ x = x
@[simp]
theorem sdiff_top {α : Type u} {x : α} [boolean_algebra α] :
@[simp]
theorem sup_inf_inf_compl {α : Type u} {x y : α} [boolean_algebra α] :
x y x y = x
@[instance]
Equations
@[instance]
def pi.boolean_algebra {ι : Type u} {α : ι → Type v} [Π (i : ι), boolean_algebra (α i)] :
boolean_algebra (Π (i : ι), α i)
Equations