A key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.

This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.

In mathematics, a join-semilattice (or upper semilattice) is a partially ordered set that has a join (a least upper bound) for any nonempty finite subset. Dually, a meet-semilattice (or lower semilattice) is a partially ordered set which has a meet (or greatest lower bound) for any nonempty finite subset. Every join-semilattice is a meet-semilattice in the inverse order and vice versa.

Semilattices can also be defined algebraically: join and meet are associative, commutative, idempotent binary operations, and any such operation induces a partial order (and the respective inverse order) such that the result of the operation for any two elements is the least upper bound (or greatest lower bound) of the elements with respect to this partial order.

A lattice is a partially ordered set that is both a meet- and join-semilattice with respect to the same partial order. Algebraically, a lattice is a set with two associative, commutative idempotent binary operations linked by corresponding absorption laws.

### Abstract Semilattice

A lattice has both a join and a meet operation but a semilattice has only one of these operatiors.

Join and meet are associative, commutative, idempotent binary operations.

Idempotent means:

- a /\ a = a
- a \/ a = a

From which we can derive:

- a /\ (a /\ b) = a /\ b
- a \/ (a \/ b) = a \/ b

There is also a right-hand version of these.

Absorptive means:

- a \/ (a /\ b) = a /\ (a \/ b) = a

This is represented in Isabelle code (from this site) by starting with an abelian group, which gives associative and commutitive binary operation (as discussed on this page) and adds the idempotent axiom like this:

So the 'f' can represent either '/\' or '\/' depending on wheter it is an infimum (meet) or supremum (join) semilattice. A lattice is then built from one of each. |
locale semilattice = abel_semigroup + assumes idem [simp]: "f a a = a" begin lemma left_idem [simp]: "f a (f a b) = f a b" by (simp add: assoc [symmetric]) lemma right_idem [simp]: "f (f a b) b = f a b" by (simp add: assoc) end |

### Idempotent semigroup

class ab_semigroup_idem_mult = ab_semigroup_mult + assumes mult_idem: "x * x = x" |

### Semilattice

class inf = fixes inf :: "'a => 'a => 'a" (infixl "\ |

### Lattice

class lattice = semilattice_inf + semilattice_sup |

### Dual lattice

text {* Dual lattice *} lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater" by (rule class.semilattice_inf.intro, rule dual_order) (unfold_locales, simp_all add: sup_least) end |

### Introduction and Elimination Rules

infimum also known as meet (a /\ b) or greatest lower bound.

context semilattice_inf begin lemma le_infI1: "a \ |

supremum also known as the join (a \/ b) or least upper bound.

context semilattice_sup begin lemma le_supI1: "x \ |

### Equational laws

subsubsection {* Equational laws *} sublocale semilattice_inf < inf!: semilattice inf proof fix a b c show "(a \ |