# Documentation

Mathlib.Order.Booleanisation

# Adding complements to a generalized Boolean algebra #

This file embeds any generalized Boolean algebra into a Boolean algebra.

This concretely proves that any equation holding true in the theory of Boolean algebras that does not reference ᶜ also holds true in the theory of generalized Boolean algebras. Put another way, one does not need the existence of complements to prove something which does not talk about complements.

## Main declarations #

• Booleanisation: Boolean algebra containing a given generalised Boolean algebra as a sublattice.
• Booleanisation.liftLatticeHom: Boolean algebra containing a given generalised Boolean algebra as a sublattice.

## Future workl #

If mathlib ever acquires GenBoolAlg, the category of generalised Boolean algebras, then one could show that Booleanisation is the free functor from GenBoolAlg to BoolAlg.

def Booleanisation (α : Type u_2) :
Type u_2

Boolean algebra containing a given generalised Boolean algebra α as a sublattice.

This should be thought of as made of a copy of α (representing elements of α) living under another copy of α (representing complements of elements of α).

Equations
Instances For
instance Booleanisation.instDecidableEq {α : Type u_1} [] :
Equations
• Booleanisation.instDecidableEq = Sum.instDecidableEqSum
@[match_pattern]
def Booleanisation.lift {α : Type u_1} :
α

The natural inclusion a ↦ a from a generalized Boolean algebra to its generated Boolean algebra.

Equations
• Booleanisation.lift = Sum.inl
Instances For
@[match_pattern]
def Booleanisation.comp {α : Type u_1} :
α

The inclusion a ↦ aᶜ from a generalized Boolean algebra to its generated Boolean algebra.

Equations
• Booleanisation.comp = Sum.inr
Instances For
inductive Booleanisation.LE {α : Type u_1} :

The order on Booleanisation α is as follows: For a b : α,

• a ≤ b iff a ≤ b in α
• a ≤ bᶜ iff a and b are disjoint in α
• aᶜ ≤ bᶜ iff b ≤ a in α
• ¬ aᶜ ≤ b
• lift: ∀ {α : Type u_1} [inst : ] {a b : α}, a b
• comp: ∀ {α : Type u_1} [inst : ] {a b : α}, a b
• sep: ∀ {α : Type u_1} [inst : ] {a b : α},
Instances For
inductive Booleanisation.LT {α : Type u_1} :

The order on Booleanisation α is as follows: For a b : α,

• a < b iff a < b in α
• a < bᶜ iff a and b are disjoint in α
• aᶜ < bᶜ iff b < a in α
• ¬ aᶜ < b
• lift: ∀ {α : Type u_1} [inst : ] {a b : α}, a < b
• comp: ∀ {α : Type u_1} [inst : ] {a b : α}, a < b
• sep: ∀ {α : Type u_1} [inst : ] {a b : α},
Instances For
instance Booleanisation.instLE {α : Type u_1} :
LE ()

The order on Booleanisation α is as follows: For a b : α,

• a ≤ b iff a ≤ b in α
• a ≤ bᶜ iff a and b are disjoint in α
• aᶜ ≤ bᶜ iff b ≤ a in α
• ¬ aᶜ ≤ b
Equations
• Booleanisation.instLE = { le := Booleanisation.LE }
instance Booleanisation.instLT {α : Type u_1} :
LT ()

The order on Booleanisation α is as follows: For a b : α,

• a < b iff a < b in α
• a < bᶜ iff a and b are disjoint in α
• aᶜ < bᶜ iff b < a in α
• ¬ aᶜ < b
Equations
• Booleanisation.instLT = { lt := Booleanisation.LT }
instance Booleanisation.instSup {α : Type u_1} :

The supremum on Booleanisation α is as follows: For a b : α,

• a ⊔ b is a ⊔ b
• a ⊔ bᶜ is (b \ a)ᶜ
• aᶜ ⊔ b is (a \ b)ᶜ
• aᶜ ⊔ bᶜ is (a ⊓ b)ᶜ
Equations
• One or more equations did not get rendered due to their size.
instance Booleanisation.instInf {α : Type u_1} :

The infimum on Booleanisation α is as follows: For a b : α,

• a ⊓ b is a ⊓ b
• a ⊓ bᶜ is a \ b
• aᶜ ⊓ b is b \ a
• aᶜ ⊓ bᶜ is (a ⊔ b)ᶜ
Equations
• One or more equations did not get rendered due to their size.
instance Booleanisation.instBot {α : Type u_1} :

The bottom element of Booleanisation α is the bottom element of α.

Equations
• Booleanisation.instBot = { bot := }
instance Booleanisation.instTop {α : Type u_1} :

The top element of Booleanisation α is the complement of the bottom element of α.

Equations
• Booleanisation.instTop = { top := }
instance Booleanisation.instCompl {α : Type u_1} :

The complement operator on Booleanisation α sends a to aᶜ and aᶜ to a, for a : α.

Equations
• Booleanisation.instCompl = { compl := fun (x : ) => match x with | => | => }
instance Booleanisation.instSDiff {α : Type u_1} :

The difference operator on Booleanisation α is as follows: For a b : α,

• a \ b is a \ b
• a \ bᶜ is a ⊓ b
• aᶜ \ b is (a ⊔ b)ᶜ
• aᶜ \ bᶜ is b \ a`
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Booleanisation.lift_le_lift {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.comp_le_comp {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.lift_le_comp {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.not_comp_le_lift {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.lift_lt_lift {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.comp_lt_comp {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.lift_lt_comp {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.not_comp_lt_lift {α : Type u_1} {a : α} {b : α} :
@[simp]
theorem Booleanisation.lift_sup_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.lift_sup_comp {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_sup_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_sup_comp {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.lift_inf_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.lift_inf_comp {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_inf_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_inf_comp {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.lift_bot {α : Type u_1} :
@[simp]
theorem Booleanisation.comp_bot {α : Type u_1} :
@[simp]
theorem Booleanisation.compl_lift {α : Type u_1} (a : α) :
@[simp]
theorem Booleanisation.compl_comp {α : Type u_1} (a : α) :
@[simp]
theorem Booleanisation.lift_sdiff_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.lift_sdiff_comp {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_sdiff_lift {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem Booleanisation.comp_sdiff_comp {α : Type u_1} (a : α) (b : α) :
instance Booleanisation.instPreorder {α : Type u_1} :
Equations
• Booleanisation.instPreorder = Preorder.mk (_ : ∀ (x : ), x x) (_ : ∀ (x y z : ), x yy zx z)
Equations
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.
Equations
Equations
• Booleanisation.instBoundedOrder = BoundedOrder.mk
Equations
• One or more equations did not get rendered due to their size.

The embedding from a generalised Boolean algebra to its generated Boolean algebra.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Booleanisation.liftLatticeHom_injective {α : Type u_1} :
Function.Injective Booleanisation.liftLatticeHom