mathlib documentation

order.boolean_algebra

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

Set / lattice complement

Instances
@[instance]
def boolean_algebra.to_has_sdiff (α : Type u_1) [s : boolean_algebra α] :

@[instance]
def boolean_algebra.to_has_compl (α : Type u_1) [s : boolean_algebra α] :

@[class]
structure boolean_algebra  :
Type u_1Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • top : α
  • le_top : ∀ (a : α), a
  • bot : α
  • bot_le : ∀ (a : α), a
  • compl : α → α
  • sdiff : α → α → α
  • 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 complementation operation - such that x ⊓ - x = ⊥ and x ⊔ - x = ⊤. This is a generalization of (classical) logic of propositions, or the powerset lattice.

Instances
@[simp]
theorem inf_compl_eq_bot {α : Type u} {x : α} [boolean_algebra α] :

@[simp]
theorem compl_inf_eq_bot {α : Type u} {x : α} [boolean_algebra α] :

@[simp]
theorem sup_compl_eq_top {α : Type u} {x : α} [boolean_algebra α] :

@[simp]
theorem compl_sup_eq_top {α : Type u} {x : α} [boolean_algebra α] :

theorem is_compl_compl {α : Type u} {x : α} [boolean_algebra α] :

theorem is_compl.compl_eq {α : Type u} {x y : α} [boolean_algebra α] :
is_compl x yx = y

theorem sdiff_eq {α : Type u} {x y : α} [boolean_algebra α] :
x \ y = x y

theorem compl_unique {α : Type u} {x y : α} [boolean_algebra α] :
x y = x y = x = y

@[simp]
theorem compl_top {α : Type u} [boolean_algebra α] :

@[simp]
theorem compl_bot {α : Type u} [boolean_algebra α] :

@[simp]
theorem compl_compl' {α : Type u} {x : α} [boolean_algebra α] :

@[simp]
theorem compl_inj_iff {α : Type u} {x y : α} [boolean_algebra α] :
x = y x = y

@[simp]
theorem compl_inf {α : Type u} {x y : α} [boolean_algebra α] :
(x y) = x y

@[simp]
theorem compl_sup {α : Type u} {x y : α} [boolean_algebra α] :
(x y) = x y

theorem compl_le_compl {α : Type u} {x y : α} [boolean_algebra α] :
y xx y

theorem compl_le_compl_iff_le {α : Type u} {x y : α} [boolean_algebra α] :
y x x y

theorem le_compl_of_le_compl {α : Type u} {x y : α} [boolean_algebra α] :
y xx y

theorem compl_le_of_compl_le {α : Type u} {x y : α} [boolean_algebra α] :
y xx y

theorem compl_le_iff_compl_le {α : Type u} {x y : α} [boolean_algebra α] :
y x x y

theorem sup_sdiff_same {α : Type u} {x y : α} [boolean_algebra α] :
x y \ x = x y

theorem sdiff_eq_left {α : Type u} {x y : α} [boolean_algebra α] :
x y = x \ y = x

theorem sdiff_le_sdiff {α : Type u} {w x y z : α} [boolean_algebra α] :
w yz xw \ x y \ z

@[instance]

Equations
@[instance]
def pi.boolean_algebra {α : Type u} {β : Type v} [boolean_algebra β] :
boolean_algebra (α → β)

Equations