Basic properties of Boolean algebras

This file provides some basic definitions, functions as well as lemmas for functions and type classes related to Boolean algebras as defined in Mathlib/Order/BooleanAlgebra/Defs.lean.

References

• https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations
• [Postulates for Boolean Algebras and Generalized Boolean Algebras, M.H. Stone][Stone1935]
• [Lattice Theory: Foundation, George Grätzer][Gratzer2011]

Tags

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

Generalized Boolean algebras

Some of the lemmas in this section are from:

• [Lattice Theory: Foundation, George Grätzer][Gratzer2011]
• https://ncatlab.org/nlab/show/relative+complement
• https://people.math.gatech.edu/~mccuan/courses/4317/symmetricdifference.pdf

@[simp]

theorem sup_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x ⊓ y ⊔ x \ y = x

@[simp]

theorem inf_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x ⊓ y ⊓ x \ y = ⊥

@[simp]

theorem sup_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x \ y ⊔ x ⊓ y = x

@[simp]

theorem inf_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x \ y ⊓ (x ⊓ y) = ⊥

@[instance 100]

instance GeneralizedBooleanAlgebra.toOrderBot {α : Type u} [GeneralizedBooleanAlgebra α] : OrderBot α

theorem disjoint_inf_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : Disjoint (x ⊓ y) (x \ y)

theorem sdiff_unique {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) : x \ y = z

@[simp]

theorem sdiff_inf_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y ⊓ y \ x = ⊥

theorem disjoint_sdiff_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : Disjoint (x \ y) (y \ x)

@[simp]

theorem inf_sdiff_self_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x ⊓ y \ x = ⊥

@[simp]

theorem inf_sdiff_self_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : y \ x ⊓ x = ⊥

@[instance 100]

instance GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra {α : Type u} [GeneralizedBooleanAlgebra α] : GeneralizedCoheytingAlgebra α

theorem disjoint_sdiff_self_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : Disjoint (y \ x) x

theorem disjoint_sdiff_self_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : Disjoint x (y \ x)

theorem le_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z

@[simp]

theorem sdiff_eq_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y = x ↔ Disjoint x y

theorem Disjoint.sdiff_eq_of_sup_eq {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hi : Disjoint x z) (hs : x ⊔ z = y) : y \ x = z

theorem Disjoint.sdiff_unique {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hd : Disjoint x z) (hz : z ≤ y) (hs : y ≤ x ⊔ z) : y \ x = z

theorem disjoint_sdiff_iff_le {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) : Disjoint z (y \ x) ↔ z ≤ x

theorem le_iff_disjoint_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) : z ≤ x ↔ Disjoint z (y \ x)

theorem inf_sdiff_eq_bot_iff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ x = ⊥ ↔ z ≤ x

theorem le_iff_eq_sup_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) : x ≤ z ↔ y = z ⊔ y \ x

theorem sdiff_sup {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : y \ (x ⊔ z) = y \ x ⊓ y \ z

theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : y \ x = y \ z ↔ y ⊓ x = y ⊓ z

theorem sdiff_eq_self_iff_disjoint {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y = x ↔ Disjoint y x

@[deprecated sdiff_eq_left (since := "2025-10-12")]

theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y = x ↔ Disjoint x y

Alias of sdiff_eq_left.

theorem sdiff_lt {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] (hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x

theorem sdiff_lt_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y < x ↔ ¬Disjoint y x

@[simp]

theorem le_sdiff_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x ≤ y \ x ↔ x = ⊥

@[simp]

theorem sdiff_eq_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y = y ↔ x = ⊥ ∧ y = ⊥

theorem sdiff_ne_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥

theorem sdiff_lt_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : x < y) (hz : z ≤ x) : x \ z < y \ z

theorem sup_inf_inf_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z

theorem sdiff_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z

theorem sdiff_sdiff_right' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : x \ (y \ z) = x \ y ⊔ x ⊓ z

theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : z ≤ x) : x \ (y \ z) = x \ y ⊔ z

@[simp]

theorem sdiff_sdiff_right_self {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ (x \ y) = x ⊓ y

theorem sdiff_sdiff_eq_self {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] (h : y ≤ x) : x \ (x \ y) = y

theorem sdiff_eq_symm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hy : y ≤ x) (h : x \ y = z) : x \ z = y

theorem sdiff_eq_comm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hy : y ≤ x) (hz : z ≤ x) : x \ y = z ↔ x \ z = y

theorem eq_of_sdiff_eq_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) : x = y

theorem sdiff_le_sdiff_iff_le {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hx : x ≤ z) (hy : y ≤ z) : z \ x ≤ z \ y ↔ y ≤ x

theorem sdiff_sdiff_left' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : (x \ y) \ z = x \ y ⊓ x \ z

theorem sdiff_sdiff_sup_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y

theorem sdiff_sdiff_sdiff_cancel_left {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hca : z ≤ x) : (x \ y) \ (x \ z) = z \ y

theorem sdiff_sdiff_sdiff_cancel_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y

theorem inf_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : (x ⊓ y) \ z = x \ z ⊓ y \ z

theorem inf_sdiff_assoc {α : Type u} [GeneralizedBooleanAlgebra α] (x y z : α) : (x ⊓ y) \ z = x ⊓ y \ z

See also sdiff_inf_right_comm.

theorem sdiff_inf_right_comm {α : Type u} [GeneralizedBooleanAlgebra α] (x y z : α) : x \ z ⊓ y = (x ⊓ y) \ z

See also inf_sdiff_assoc.

theorem inf_sdiff_left_comm {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) : a ⊓ b \ c = b ⊓ a \ c

theorem inf_sdiff_distrib_left {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

theorem inf_sdiff_distrib_right {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

theorem disjoint_sdiff_comm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] : Disjoint (x \ z) y ↔ Disjoint x (y \ z)

theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y

theorem sup_lt_of_lt_sdiff_left {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : y < z \ x) (hxz : x ≤ z) : x ⊔ y < z

theorem sup_lt_of_lt_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : x < z \ y) (hyz : y ≤ z) : x ⊔ y < z

instance Prod.instGeneralizedBooleanAlgebra {α : Type u} {β : Type u_1} [GeneralizedBooleanAlgebra α] [GeneralizedBooleanAlgebra β] : GeneralizedBooleanAlgebra (α × β)

instance Pi.instGeneralizedBooleanAlgebra {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → GeneralizedBooleanAlgebra (α i)] : GeneralizedBooleanAlgebra ((i : ι) → α i)

Boolean algebras

@[reducible, inline]

abbrev GeneralizedBooleanAlgebra.toBooleanAlgebra {α : Type u} [GeneralizedBooleanAlgebra α] [OrderTop α] : BooleanAlgebra α

A bounded generalized Boolean algebra is a Boolean algebra.

theorem inf_compl_eq_bot' {α : Type u} {x : α} [BooleanAlgebra α] : x ⊓ xᶜ = ⊥

@[simp]

theorem sup_compl_eq_top {α : Type u} {x : α} [BooleanAlgebra α] : x ⊔ xᶜ = ⊤

@[simp]

theorem compl_sup_eq_top {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ ⊔ x = ⊤

theorem isCompl_compl {α : Type u} {x : α} [BooleanAlgebra α] : IsCompl x xᶜ

theorem sdiff_eq {α : Type u} {x y : α} [BooleanAlgebra α] : x \ y = x ⊓ yᶜ

theorem himp_eq {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y = y ⊔ xᶜ

@[instance 100]

instance BooleanAlgebra.toComplementedLattice {α : Type u} [BooleanAlgebra α] : ComplementedLattice α

@[instance 100]

instance BooleanAlgebra.toGeneralizedBooleanAlgebra {α : Type u} [BooleanAlgebra α] : GeneralizedBooleanAlgebra α

@[instance 100]

instance BooleanAlgebra.toBiheytingAlgebra {α : Type u} [BooleanAlgebra α] : BiheytingAlgebra α

@[simp]

theorem hnot_eq_compl {α : Type u} {x : α} [BooleanAlgebra α] : ￢x = xᶜ

theorem top_sdiff {α : Type u} {x : α} [BooleanAlgebra α] : ⊤ \ x = xᶜ

theorem eq_compl_iff_isCompl {α : Type u} {x y : α} [BooleanAlgebra α] : x = yᶜ ↔ IsCompl x y

theorem compl_eq_iff_isCompl {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ = y ↔ IsCompl x y

theorem compl_eq_comm {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ = y ↔ yᶜ = x

theorem eq_compl_comm {α : Type u} {x y : α} [BooleanAlgebra α] : x = yᶜ ↔ y = xᶜ

@[simp]

theorem compl_compl {α : Type u} [BooleanAlgebra α] (x : α) : xᶜᶜ = x

theorem compl_comp_compl {α : Type u} [BooleanAlgebra α] : compl ∘ compl = id

@[simp]

theorem compl_involutive {α : Type u} [BooleanAlgebra α] : Function.Involutive compl

theorem compl_bijective {α : Type u} [BooleanAlgebra α] : Function.Bijective compl

theorem compl_surjective {α : Type u} [BooleanAlgebra α] : Function.Surjective compl

theorem compl_injective {α : Type u} [BooleanAlgebra α] : Function.Injective compl

@[simp]

theorem compl_inj_iff {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ = yᶜ ↔ x = y

theorem IsCompl.compl_eq_iff {α : Type u} {x y z : α} [BooleanAlgebra α] (h : IsCompl x y) : zᶜ = y ↔ z = x

@[simp]

theorem compl_eq_top {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ = ⊤ ↔ x = ⊥

@[simp]

theorem compl_eq_bot {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ = ⊥ ↔ x = ⊤

@[simp]

theorem compl_inf {α : Type u} {x y : α} [BooleanAlgebra α] : (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ

@[simp]

theorem compl_le_compl_iff_le {α : Type u} {x y : α} [BooleanAlgebra α] : yᶜ ≤ xᶜ ↔ x ≤ y

@[simp]

theorem compl_lt_compl_iff_lt {α : Type u} {x y : α} [BooleanAlgebra α] : yᶜ < xᶜ ↔ x < y

theorem compl_le_of_compl_le {α : Type u} {x y : α} [BooleanAlgebra α] (h : yᶜ ≤ x) : xᶜ ≤ y

theorem compl_le_iff_compl_le {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ ≤ y ↔ yᶜ ≤ x

@[simp]

theorem compl_le_self {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ ≤ x ↔ x = ⊤

@[simp]

theorem compl_lt_self {α : Type u} {x : α} [BooleanAlgebra α] [Nontrivial α] : xᶜ < x ↔ x = ⊤

@[simp]

theorem sdiff_compl {α : Type u} {x y : α} [BooleanAlgebra α] : x \ yᶜ = x ⊓ y

instance OrderDual.instBooleanAlgebra {α : Type u} [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ

@[simp]

theorem sup_inf_inf_compl {α : Type u} {x y : α} [BooleanAlgebra α] : x ⊓ y ⊔ x ⊓ yᶜ = x

theorem compl_sdiff {α : Type u} {x y : α} [BooleanAlgebra α] : (x \ y)ᶜ = x ⇨ y

@[simp]

theorem compl_himp {α : Type u} {x y : α} [BooleanAlgebra α] : (x ⇨ y)ᶜ = x \ y

theorem compl_sdiff_compl {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ \ yᶜ = y \ x

@[simp]

theorem compl_himp_compl {α : Type u} {x y : α} [BooleanAlgebra α] : xᶜ ⇨ yᶜ = y ⇨ x

theorem disjoint_compl_left_iff {α : Type u} {x y : α} [BooleanAlgebra α] : Disjoint xᶜ y ↔ y ≤ x

theorem disjoint_compl_right_iff {α : Type u} {x y : α} [BooleanAlgebra α] : Disjoint x yᶜ ↔ x ≤ y

theorem codisjoint_himp_self_left {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint (x ⇨ y) x

theorem codisjoint_himp_self_right {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint x (x ⇨ y)

theorem himp_le {α : Type u} {x y z : α} [BooleanAlgebra α] : x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z

@[simp]

theorem himp_le_left {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≤ x ↔ x = ⊤

@[simp]

theorem himp_eq_left {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤

theorem himp_ne_right {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤

theorem codisjoint_iff_compl_le_left {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint x y ↔ yᶜ ≤ x

theorem codisjoint_iff_compl_le_right {α : Type u} {x y : α} [BooleanAlgebra α] : Codisjoint x y ↔ xᶜ ≤ y

instance Prod.instBooleanAlgebra {α : Type u} {β : Type u_1} [BooleanAlgebra α] [BooleanAlgebra β] : BooleanAlgebra (α × β)

instance Pi.instBooleanAlgebra {ι : Type u} {α : ι → Type v} [(i : ι) → BooleanAlgebra (α i)] : BooleanAlgebra ((i : ι) → α i)

@[reducible, inline]

abbrev Function.Injective.generalizedBooleanAlgebra {α : Type u} {β : Type u_1} [Max α] [Min α] [LE α] [LT α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (f : α → β) (hf : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (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) : GeneralizedBooleanAlgebra α

Pullback a GeneralizedBooleanAlgebra along an injection.

@[reducible, inline]

abbrev Function.Injective.booleanAlgebra {α : Type u} {β : Type u_1} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (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) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : BooleanAlgebra α

Pullback a BooleanAlgebra along an injection.