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:

source
@[instance]
def generalized_boolean_algebra.to_has_bot (α : Type u) [self : generalized_boolean_algebra α] :
has_bot α
source
@[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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
  • le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
  • sdiff : α → α → α
  • bot : α
  • 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
source
@[instance]
def generalized_boolean_algebra.to_distrib_lattice (α : Type u) [self : generalized_boolean_algebra α] :
distrib_lattice α
source
@[instance]
def generalized_boolean_algebra.to_has_sdiff (α : Type u) [self : generalized_boolean_algebra α] :
has_sdiff α
source
@[simp]
theorem sup_inf_sdiff {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x ⊓ y ⊔ x \ y = x
source
@[simp]
theorem inf_inf_sdiff {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x ⊓ y ⊓ x \ y = ⊥
source
@[simp]
theorem sup_sdiff_inf {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x \ y ⊔ x ⊓ y = x
source
@[simp]
theorem inf_sdiff_inf {α : Type u} [generalized_boolean_algebra α] (x y : α) :
x \ y ⊓ (x ⊓ y) = ⊥
source
@[protected, instance]
def generalized_boolean_algebra.to_order_bot {α : Type u} [generalized_boolean_algebra α] :
order_bot α
Equations
source
theorem disjoint_inf_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (x ⊓ y) (x \ y)
source
theorem sdiff_unique {α : Type u} {x y z : α} [generalized_boolean_algebra α] (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) :
x \ y = z
source
theorem sdiff_le {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y ≤ x
source
@[simp]
theorem bot_sdiff {α : Type u} {x : α} [generalized_boolean_algebra α] :
⊥ \ x = ⊥
source
theorem inf_sdiff_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊓ x \ y = x \ y
source
theorem inf_sdiff_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y ⊓ x = x \ y
source
@[simp]
theorem sdiff_self {α : Type u} {x : α} [generalized_boolean_algebra α] :
x \ x = ⊥
source
@[simp]
theorem sup_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊔ y \ x = x ⊔ y
source
@[simp]
theorem sup_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x ⊔ x = y ⊔ x
source
theorem sup_sdiff_symm {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊔ y \ x = y ⊔ x \ y
source
theorem sup_sdiff_cancel_right {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : x ≤ y) :
x ⊔ y \ x = y
source
theorem sdiff_sup_cancel {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : y ≤ x) :
x \ y ⊔ y = x
source
theorem sup_le_of_le_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : y ≤ z \ x) (hxz : x ≤ z) :
x ⊔ y ≤ z
source
theorem sup_le_of_le_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : x ≤ z \ y) (hyz : y ≤ z) :
x ⊔ y ≤ z
source
@[simp]
theorem sup_sdiff_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊔ x \ y = x
source
theorem sup_sdiff_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y ⊔ x = x
source
@[simp]
theorem sdiff_inf_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y ⊓ y \ x = ⊥
source
theorem disjoint_sdiff_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (x \ y) (y \ x)
source
theorem le_sup_sdiff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y ≤ x ⊔ y \ x
source
theorem le_sdiff_sup {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y ≤ y \ x ⊔ x
source
@[simp]
theorem inf_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊓ y \ x = ⊥
source
@[simp]
theorem inf_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x ⊓ x = ⊥
source
theorem disjoint_sdiff_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint (y \ x) x
source
theorem disjoint_sdiff_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
disjoint x (y \ x)
source
theorem disjoint.disjoint_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : disjoint x y) :
disjoint (x \ z) y
source
theorem disjoint.disjoint_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : disjoint x y) :
disjoint x (y \ z)
source
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
source
theorem disjoint.sup_sdiff_cancel_left {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
(x ⊔ y) \ x = y
source
theorem disjoint.sup_sdiff_cancel_right {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
(x ⊔ y) \ y = x
source
@[protected]
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
source
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
source
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)
source
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
source
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
source
theorem sup_sdiff_cancel' {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hx : x ≤ z) (hz : z ≤ y) :
z ⊔ y \ x = y
source
theorem sdiff_sup {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ (x ⊔ z) = y \ x ⊓ y \ z
source
theorem sdiff_inf {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ (x ⊓ z) = y \ x ⊔ y \ z
source
@[simp]
theorem sdiff_inf_self_right {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ (x ⊓ y) = y \ x
source
@[simp]
theorem sdiff_inf_self_left {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ (y ⊓ x) = y \ x
source
theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ x = y \ z ↔ y ⊓ x = y ⊓ z
source
theorem disjoint.sdiff_eq_left {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
x \ y = x
source
theorem disjoint.sdiff_eq_right {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : disjoint x y) :
y \ x = y
source
@[simp]
theorem sdiff_bot {α : Type u} {x : α} [generalized_boolean_algebra α] :
x \ ⊥ = x
source
theorem sdiff_eq_self_iff_disjoint {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y = x ↔ disjoint y x
source
theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y = x ↔ disjoint x y
source
theorem sdiff_lt {α : Type u} {x y : α} [generalized_boolean_algebra α] (hx : y ≤ x) (hy : y ≠ ⊥) :
x \ y < x
source
theorem sdiff_le_sdiff_left {α : Type u} {w x z : α} [generalized_boolean_algebra α] (h : z ≤ x) :
w \ x ≤ w \ z
source
theorem sdiff_le_iff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
y \ x ≤ z ↔ y ≤ x ⊔ z
source
theorem sdiff_sdiff_le {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ (x \ y) ≤ y
source
@[simp]
theorem le_sdiff_iff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ≤ y \ x ↔ x = ⊥
source
@[simp]
theorem sdiff_eq_bot_iff {α : Type u} {x y : α} [generalized_boolean_algebra α] :
y \ x = ⊥ ↔ y ≤ x
source
theorem sdiff_le_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y ≤ z ↔ x \ z ≤ y
source
theorem sdiff_le_sdiff_right {α : Type u} {w x y : α} [generalized_boolean_algebra α] (h : w ≤ y) :
w \ x ≤ y \ x
source
theorem sdiff_le_sdiff {α : Type u} {w x y z : α} [generalized_boolean_algebra α] (h₁ : w ≤ y) (h₂ : z ≤ x) :
w \ x ≤ y \ z
source
theorem sdiff_lt_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : x < y) (hz : z ≤ x) :
x \ z < y \ z
source
theorem sup_inf_inf_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
source
@[simp]
theorem inf_sdiff_sup_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ z ⊓ (x ⊔ y) = x \ z
source
@[simp]
theorem inf_sdiff_sup_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ z ⊓ (y ⊔ x) = x \ z
source
theorem sdiff_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
source
theorem sdiff_sdiff_right' {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ (y \ z) = x \ y ⊔ x ⊓ z
source
theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : z ≤ x) :
x \ (y \ z) = x \ y ⊔ z
source
@[simp]
theorem sdiff_sdiff_right_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ (x \ y) = x ⊓ y
source
theorem sdiff_sdiff_eq_self {α : Type u} {x y : α} [generalized_boolean_algebra α] (h : y ≤ x) :
x \ (x \ y) = y
source
theorem sdiff_eq_symm {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hy : y ≤ x) (h : x \ y = z) :
x \ z = y
source
theorem sdiff_eq_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hy : y ≤ x) (hz : z ≤ x) :
x \ y = z ↔ x \ z = y
source
theorem eq_of_sdiff_eq_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) :
x = y
source
theorem sdiff_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ (y ⊔ z)
source
theorem sdiff_sdiff_left' {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ y ⊓ x \ z
source
theorem sdiff_sdiff_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ y \ z = x \ z \ y
source
@[simp]
theorem sdiff_idem {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y \ y = x \ y
source
@[simp]
theorem sdiff_sdiff_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x \ y \ x = ⊥
source
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)
source
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
source
theorem sup_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
(x ⊔ y) \ z = x \ z ⊔ y \ z
source
theorem sup_sdiff_right_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
(x ⊔ y) \ y = x \ y
source
theorem sup_sdiff_left_self {α : Type u} {x y : α} [generalized_boolean_algebra α] :
(x ⊔ y) \ x = y \ x
source
theorem inf_sdiff {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
(x ⊓ y) \ z = x \ z ⊓ y \ z
source
theorem inf_sdiff_assoc {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
(x ⊓ y) \ z = x ⊓ y \ z
source
theorem inf_sdiff_right_comm {α : Type u} {x y z : α} [generalized_boolean_algebra α] :
x \ z ⊓ y = (x ⊓ y) \ z
source
theorem inf_sdiff_distrib_left {α : Type u} [generalized_boolean_algebra α] (a b c : α) :
a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
source
theorem inf_sdiff_distrib_right {α : Type u} [generalized_boolean_algebra α] (a b c : α) :
a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
source
theorem sdiff_sup_sdiff_cancel {α : Type u} {x y z : α} [generalized_boolean_algebra α] (hyx : y ≤ x) (hzy : z ≤ y) :
x \ y ⊔ y \ z = x \ z
source
theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x y : α} [generalized_boolean_algebra α] :
x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y
source
theorem sdiff_le_sdiff_of_sup_le_sup_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : z ⊔ x ≤ z ⊔ y) :
x \ z ≤ y \ z
source
theorem sdiff_le_sdiff_of_sup_le_sup_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : x ⊔ z ≤ y ⊔ z) :
x \ z ≤ y \ z
source
theorem sup_lt_of_lt_sdiff_left {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : y < z \ x) (hxz : x ≤ z) :
x ⊔ y < z
source
theorem sup_lt_of_lt_sdiff_right {α : Type u} {x y z : α} [generalized_boolean_algebra α] (h : x < z \ y) (hyz : y ≤ z) :
x ⊔ y < z
source
@[protected, instance]
def pi.generalized_boolean_algebra {α : Type u} {β : Type v} [generalized_boolean_algebra β] :
generalized_boolean_algebra (α → β)
Equations

Boolean algebras #

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

Set / lattice complement

Instances
source
@[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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
  • le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
  • compl : α → α
  • top : α
  • bot : α
  • inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
  • top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ
  • le_top : ∀ (a : α), a ≤ ⊤
  • bot_le : ∀ (a : α), ⊥ ≤ a

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

Since bounded_order, order_bot, and order_top are mixins that require has_le to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying has_bot and has_top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to bounded_order is provided.

Instances
source
@[instance]
def boolean_algebra.core.to_has_bot (α : Type u) [self : boolean_algebra.core α] :
has_bot α
source
@[instance]
def boolean_algebra.core.to_has_top (α : Type u) [self : boolean_algebra.core α] :
has_top α
source
@[instance]
def boolean_algebra.core.to_has_compl (α : Type u) [self : boolean_algebra.core α] :
has_compl α
source
@[instance]
def boolean_algebra.core.to_distrib_lattice (α : Type u) [self : boolean_algebra.core α] :
distrib_lattice α
source
@[protected, instance]
def boolean_algebra.core.to_bounded_order {α : Type u} [h : boolean_algebra.core α] :
bounded_order α
Equations
source
@[simp]
theorem inf_compl_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
x ⊓ xᶜ = ⊥
source
@[simp]
theorem compl_inf_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
xᶜ ⊓ x = ⊥
source
@[simp]
theorem sup_compl_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
x ⊔ xᶜ = ⊤
source
@[simp]
theorem compl_sup_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
xᶜ ⊔ x = ⊤
source
theorem is_compl_compl {α : Type u} {x : α} [boolean_algebra.core α] :
is_compl x xᶜ
source
theorem is_compl.eq_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : is_compl x y) :
x = yᶜ
source
theorem is_compl.compl_eq {α : Type u} {x y : α} [boolean_algebra.core α] (h : is_compl x y) :
xᶜ = y
source
theorem eq_compl_iff_is_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
x = yᶜ ↔ is_compl x y
source
theorem compl_eq_iff_is_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
xᶜ = y ↔ is_compl x y
source
theorem disjoint_compl_right {α : Type u} {x : α} [boolean_algebra.core α] :
disjoint x xᶜ
source
theorem disjoint_compl_left {α : Type u} {x : α} [boolean_algebra.core α] :
disjoint xᶜ x
source
theorem compl_unique {α : Type u} {x y : α} [boolean_algebra.core α] (i : x ⊓ y = ⊥) (s : x ⊔ y = ⊤) :
xᶜ = y
source
@[simp]
theorem compl_top {α : Type u} [boolean_algebra.core α] :
⊤ᶜ = ⊥
source
@[simp]
theorem compl_bot {α : Type u} [boolean_algebra.core α] :
⊥ᶜ = ⊤
source
@[simp]
theorem compl_compl {α : Type u} [boolean_algebra.core α] (x : α) :
xᶜᶜ = x
source
@[simp]
theorem compl_involutive {α : Type u} [boolean_algebra.core α] :
function.involutive compl
source
theorem compl_bijective {α : Type u} [boolean_algebra.core α] :
function.bijective compl
source
theorem compl_surjective {α : Type u} [boolean_algebra.core α] :
function.surjective compl
source
theorem compl_injective {α : Type u} [boolean_algebra.core α] :
function.injective compl
source
@[simp]
theorem compl_inj_iff {α : Type u} {x y : α} [boolean_algebra.core α] :
xᶜ = yᶜ ↔ x = y
source
theorem is_compl.compl_eq_iff {α : Type u} {x y z : α} [boolean_algebra.core α] (h : is_compl x y) :
zᶜ = y ↔ z = x
source
@[simp]
theorem compl_eq_top {α : Type u} {x : α} [boolean_algebra.core α] :
xᶜ = ⊤ ↔ x = ⊥
source
@[simp]
theorem compl_eq_bot {α : Type u} {x : α} [boolean_algebra.core α] :
xᶜ = ⊥ ↔ x = ⊤
source
@[simp]
theorem compl_inf {α : Type u} {x y : α} [boolean_algebra.core α] :
(x ⊓ y)ᶜ = xᶜ ⊔ yᶜ
source
@[simp]
theorem compl_sup {α : Type u} {x y : α} [boolean_algebra.core α] :
(x ⊔ y)ᶜ = xᶜ ⊓ yᶜ
source
theorem compl_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : y ≤ x) :
xᶜ ≤ yᶜ
source
@[simp]
theorem compl_le_compl_iff_le {α : Type u} {x y : α} [boolean_algebra.core α] :
yᶜ ≤ xᶜ ↔ x ≤ y
source
theorem le_compl_of_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] (h : y ≤ xᶜ) :
x ≤ yᶜ
source
theorem compl_le_of_compl_le {α : Type u} {x y : α} [boolean_algebra.core α] (h : yᶜ ≤ x) :
xᶜ ≤ y
source
theorem le_compl_iff_le_compl {α : Type u} {x y : α} [boolean_algebra.core α] :
y ≤ xᶜ ↔ x ≤ yᶜ
source
theorem compl_le_iff_compl_le {α : Type u} {x y : α} [boolean_algebra.core α] :
xᶜ ≤ y ↔ yᶜ ≤ x
source
@[protected, instance]
def boolean_algebra.is_complemented {α : Type u} [boolean_algebra.core α] :
is_complemented α
source
@[instance]
def boolean_algebra.to_core (α : Type u) [self : boolean_algebra α] :
boolean_algebra.core α
source
@[instance]
def boolean_algebra.to_generalized_boolean_algebra (α : Type u) [self : boolean_algebra α] :
generalized_boolean_algebra α
source
@[class]
structure boolean_algebra (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
  • le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
  • sdiff : α → α → α
  • bot : α
  • sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a
  • inf_inf_sdiff : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥
  • compl : α → α
  • top : α
  • inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
  • top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ
  • le_top : ∀ (a : α), a ≤ ⊤
  • bot_le : ∀ (a : α), ⊥ ≤ a
  • 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
source
def boolean_algebra.core.sdiff {α : Type u} [boolean_algebra.core α] :
has_sdiff α

Create a has_sdiff 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.

See note [reducible non-instances].

Equations
source
theorem boolean_algebra.core.sdiff_eq {α : Type u} [boolean_algebra.core α] (a b : α) :
a \ b = a ⊓ bᶜ
source
def boolean_algebra.of_core {α : Type u} (B : boolean_algebra.core α) :
boolean_algebra α

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
source
@[protected, instance]
def order_dual.boolean_algebra {α : Type u} [boolean_algebra α] :
boolean_algebra (order_dual α)
Equations
source
theorem sdiff_eq {α : Type u} {x y : α} [boolean_algebra α] :
x \ y = x ⊓ yᶜ
source
@[simp]
theorem sdiff_compl {α : Type u} {x y : α} [boolean_algebra α] :
x \ yᶜ = x ⊓ y
source
@[simp]
theorem top_sdiff {α : Type u} {x : α} [boolean_algebra α] :
⊤ \ x = xᶜ
source
@[simp]
theorem sdiff_top {α : Type u} {x : α} [boolean_algebra α] :
x \ ⊤ = ⊥
source
@[simp]
theorem sup_inf_inf_compl {α : Type u} {x y : α} [boolean_algebra α] :
x ⊓ y ⊔ x ⊓ yᶜ = x
source
@[simp]
theorem compl_sdiff {α : Type u} {x y : α} [boolean_algebra α] :
(x \ y)ᶜ = xᶜ ⊔ y
source
@[protected, instance]
def Prop.boolean_algebra  :
boolean_algebra Prop
Equations
source
@[protected, instance]
def pi.has_sdiff {ι : Type u} {α : ι → Type v} [Π (i : ι), has_sdiff (α i)] :
has_sdiff (Π (i : ι), α i)
Equations
source
theorem pi.sdiff_def {ι : Type u} {α : ι → Type v} [Π (i : ι), has_sdiff (α i)] (x y : Π (i : ι), α i) :
x \ y = λ (i : ι), x i \ y i
source
@[simp]
theorem pi.sdiff_apply {ι : Type u} {α : ι → Type v} [Π (i : ι), has_sdiff (α i)] (x y : Π (i : ι), α i) (i : ι) :
(x \ y) i = x i \ y i
source
@[protected, instance]
def pi.has_compl {ι : Type u} {α : ι → Type v} [Π (i : ι), has_compl (α i)] :
has_compl (Π (i : ι), α i)
Equations
source
theorem pi.compl_def {ι : Type u} {α : ι → Type v} [Π (i : ι), has_compl (α i)] (x : Π (i : ι), α i) :
xᶜ = λ (i : ι), (x i)ᶜ
source
@[simp]
theorem pi.compl_apply {ι : Type u} {α : ι → Type v} [Π (i : ι), has_compl (α i)] (x : Π (i : ι), α i) (i : ι) :
xᶜ i = (x i)ᶜ
source
@[protected, instance]
def pi.boolean_algebra {ι : Type u} {α : ι → Type v} [Π (i : ι), boolean_algebra (α i)] :
boolean_algebra (Π (i : ι), α i)
Equations
source
@[protected, instance]
def bool.boolean_algebra  :
boolean_algebra bool
Equations
source
@[protected]
def function.injective.generalized_boolean_algebra {α : Type u} {β : Type u_1} [has_sup α] [has_inf α] [has_bot α] [has_sdiff α] [generalized_boolean_algebra β] (f : α → β) (hf : function.injective f) (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) :
generalized_boolean_algebra α

Pullback a generalized_boolean_algebra along an injection.

Equations
source
@[protected]
def function.injective.boolean_algebra {α : Type u} {β : Type u_1} [has_sup α] [has_inf α] [has_top α] [has_bot α] [has_compl α] [has_sdiff α] [boolean_algebra β] (f : α → β) (hf : function.injective f) (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) :
boolean_algebra α

Pullback a boolean_algebra along an injection.

Equations