# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Lattice_ZF imports Order_ZF_1a func1
begin

Lattices can be introduced in algebraic way as commutative idempotent ($$x\cdot x =x$$) semigroups or as partial orders with some additional properties. These two approaches are equivalent. In this theory we will use the order-theoretic approach.

### Semilattices

We start with a relation $$r$$ which is a partial order on a set $$L$$. Such situation is defined in Order_ZF as the predicate $$\text{IsPartOrder}(L,r)$$.

A partially ordered $$(L,r)$$ set is a join-semilattice if each two-element subset of $$L$$ has a supremum (i.e. the least upper bound).

Definition

$$\text{IsJoinSemilattice}(L,r) \equiv$$ $$r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAsupremum}(r,\{x,y\}))$$

A partially ordered $$(L,r)$$ set is a meet-semilattice if each two-element subset of $$L$$ has an infimum (i.e. the greatest lower bound).

Definition

$$\text{IsMeetSemilattice}(L,r) \equiv$$ $$r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAnInfimum}(r,\{x,y\}))$$

A partially ordered $$(L,r)$$ set is a lattice if it is both join and meet-semilattice, i.e. if every two element set has a supremum (least upper bound) and infimum (greatest lower bound).

Definition

$$r \text{ is a lattice on } L \equiv \text{IsJoinSemilattice}(L,r) \wedge \text{IsMeetSemilattice}(L,r)$$

Join is a binary operation whose value on a pair $$\langle x,y\rangle$$ is defined as the supremum of the set $$\{ x,y\}$$.

Definition

$$\text{Join}(L,r) \equiv \{\langle p, \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\}$$

Meet is a binary operation whose value on a pair $$\langle x,y\rangle$$ is defined as the infimum of the set $$\{ x,y\}$$.

Definition

$$\text{Meet}(L,r) \equiv \{\langle p, \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\}$$

Linear order is a lattice.

lemma lin_is_latt:

assumes $$r\subseteq L\times L$$ and $$\text{IsLinOrder}(L,r)$$

shows $$r \text{ is a lattice on } L$$proof
from assms(2) have $$\text{IsPartOrder}(L,r)$$ using Order_ZF_1_L2
with assms have $$\text{IsMeetSemilattice}(L,r)$$ unfolding IsLinOrder_def, IsMeetSemilattice_def using inf_sup_two_el(1)
moreover
from assms, $$\text{IsPartOrder}(L,r)$$ have $$\text{IsJoinSemilattice}(L,r)$$ unfolding IsLinOrder_def, IsJoinSemilattice_def using inf_sup_two_el(3)
ultimately show $$thesis$$ unfolding IsAlattice_def
qed

In a join-semilattice join is indeed a binary operation.

lemma join_is_binop:

assumes $$\text{IsJoinSemilattice}(L,r)$$

shows $$\text{Join}(L,r) : L\times L \rightarrow L$$proof
from assms have $$\forall p \in L\times L.\ \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\}) \in L$$ unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space
then show $$thesis$$ unfolding Join_def using ZF_fun_from_total
qed

The value of $$\text{Join}(L,r)$$ on a pair $$\langle x,y\rangle$$ is the supremum of the set $$\{ x,y\}$$, hence its is greater or equal than both.

lemma join_val:

assumes $$\text{IsJoinSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$j \equiv \text{Join}(L,r)\langle x,y\rangle$$

shows $$j\in L$$, $$j = \text{Supremum}(r,\{x,y\})$$, $$\langle x,j\rangle \in r$$, $$\langle y,j\rangle \in r$$proof
from assms(1) have $$\text{Join}(L,r) : L\times L \rightarrow L$$ using join_is_binop
with assms(2,3,4) show $$j = \text{Supremum}(r,\{x,y\})$$ unfolding Join_def using ZF_fun_from_tot_val
from assms(2,3,4), $$\text{Join}(L,r) : L\times L \rightarrow L$$ show $$j\in L$$ using apply_funtype
from assms(1,2,3) have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{HasAminimum}(r,\bigcap z\in \{x,y\}.\ r\{z\})$$ unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def
with $$j = \text{Supremum}(r,\{x,y\})$$ show $$\langle x,j\rangle \in r$$ and $$\langle y,j\rangle \in r$$ using sup_in_space(2)
qed

In a meet-semilattice meet is indeed a binary operation.

lemma meet_is_binop:

assumes $$\text{IsMeetSemilattice}(L,r)$$

shows $$\text{Meet}(L,r) : L\times L \rightarrow L$$proof
from assms have $$\forall p \in L\times L.\ \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\}) \in L$$ unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space
then show $$thesis$$ unfolding Meet_def using ZF_fun_from_total
qed

The value of $$\text{Meet}(L,r)$$ on a pair $$\langle x,y\rangle$$ is the infimum of the set $$\{ x,y\}$$, hence is less or equal than both.

lemma meet_val:

assumes $$\text{IsMeetSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$m \equiv \text{Meet}(L,r)\langle x,y\rangle$$

shows $$m\in L$$, $$m = \text{Infimum}(r,\{x,y\})$$, $$\langle m,x\rangle \in r$$, $$\langle m,y\rangle \in r$$proof
from assms(1) have $$\text{Meet}(L,r) : L\times L \rightarrow L$$ using meet_is_binop
with assms(2,3,4) show $$m = \text{Infimum}(r,\{x,y\})$$ unfolding Meet_def using ZF_fun_from_tot_val
from assms(2,3,4), $$\text{Meet}(L,r) : L\times L \rightarrow L$$ show $$m\in L$$ using apply_funtype
from assms(1,2,3) have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{HasAmaximum}(r,\bigcap z\in \{x,y\}.\ r^{-1}\{z\})$$ unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def
with $$m = \text{Infimum}(r,\{x,y\})$$ show $$\langle m,x\rangle \in r$$ and $$\langle m,y\rangle \in r$$ using inf_in_space(2)
qed

In a (nonempty) meet semi-lattice the relation down-directs the set.

lemma meet_down_directs:

assumes $$\text{IsMeetSemilattice}(L,r)$$, $$L\neq 0$$

shows $$r \text{ down-directs } L$$proof
{
fix $$x$$ $$y$$
assume $$x\in L$$, $$y\in L$$
let $$m = \text{Meet}(L,r)\langle x,y\rangle$$
from assms(1), $$x\in L$$, $$y\in L$$ have $$m\in L$$, $$\langle m,x\rangle \in r$$, $$\langle m,y\rangle \in r$$ using meet_val
}
hence $$\forall x\in L.\ \forall y\in L.\ \exists m\in L.\ \langle m,x\rangle \in r \wedge \langle m,y\rangle \in r$$
with assms(2) show $$thesis$$ unfolding DownDirects_def
qed

In a (nonempty) join semi-lattice the relation up-directs the set.

lemma join_up_directs:

assumes $$\text{IsJoinSemilattice}(L,r)$$, $$L\neq 0$$

shows $$r \text{ up-directs } L$$proof
{
fix $$x$$ $$y$$
assume $$x\in L$$, $$y\in L$$
let $$m = \text{Join}(L,r)\langle x,y\rangle$$
from assms(1), $$x\in L$$, $$y\in L$$ have $$m\in L$$, $$\langle x,m\rangle \in r$$, $$\langle y,m\rangle \in r$$ using join_val
}
hence $$\forall x\in L.\ \forall y\in L.\ \exists m\in L.\ \langle x,m\rangle \in r \wedge \langle y,m\rangle \in r$$
with assms(2) show $$thesis$$ unfolding UpDirects_def
qed

The next locale defines a a notation for join-semilattice. We will use the $$\sqcup$$ symbol rather than more common $$\vee$$ to avoid confusion with logical "or".

Locale join_semilatt

assumes joinLatt: $$\text{IsJoinSemilattice}(L,r)$$

defines $$x \sqcup y \equiv \text{Join}(L,r)\langle x,y\rangle$$

defines $$\text{sup}A \equiv \text{Supremum}(r,A)$$

Join of the elements of the lattice is in the lattice.

lemma (in join_semilatt) join_props:

assumes $$x\in L$$, $$y\in L$$

shows $$x\sqcup y \in L$$ and $$x\sqcup y = \text{sup}\{x,y\}$$proof
from joinLatt, assms have $$\text{Join}(L,r)\langle x,y\rangle \in L$$ using join_is_binop, apply_funtype
thus $$x\sqcup y \in L$$
from joinLatt, assms have $$\text{Join}(L,r)\langle x,y\rangle = \text{Supremum}(r,\{x,y\})$$ using join_val(2)
thus $$x\sqcup y = \text{sup}\{x,y\}$$
qed

Join is associative.

lemma (in join_semilatt) join_assoc:

assumes $$x\in L$$, $$y\in L$$, $$z\in L$$

shows $$x\sqcup (y\sqcup z) = x\sqcup y\sqcup z$$proof
from joinLatt, assms(2,3) have $$x\sqcup (y\sqcup z) = x\sqcup (\text{sup}\{y,z\})$$ using join_val(2)
also
from assms, joinLatt have $$.\ .\ .\ = \text{sup}\{\text{sup}\{x\}, \text{sup}\{y,z\}\}$$ unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props, sup_inf_singl(2)
also
have $$.\ .\ .\ = \text{sup}\{x,y,z\}$$proof
let $$\mathcal{T} = \{\{x\},\{y,z\}\}$$
from joinLatt have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$ unfolding IsJoinSemilattice_def, IsPartOrder_def
moreover
from joinLatt, assms have $$\forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T)$$ unfolding IsJoinSemilattice_def, IsPartOrder_def using sup_inf_singl(1)
moreover
from joinLatt, assms have $$\text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \})$$ unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space(1), sup_inf_singl(2)
ultimately have $$\text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} )$$ by (rule sup_sup )
moreover
have $$\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \} = \{\text{sup}\{x\}, \text{sup}\{y,z\}\}$$ and $$\bigcup \mathcal{T} = \{x,y,z\}$$
ultimately show $$(\text{sup}\{\text{sup}\{x\}, \text{sup}\{y,z\}\}) = \text{sup}\{x,y,z\}$$
qed
also
have $$.\ .\ .\ = \text{sup}\{\text{sup}\{x,y\}, \text{sup}\{z\}\}$$proof
let $$\mathcal{T} = \{\{x,y\},\{z\}\}$$
from joinLatt have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$ unfolding IsJoinSemilattice_def, IsPartOrder_def
moreover
from joinLatt, assms have $$\forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T)$$ unfolding IsJoinSemilattice_def, IsPartOrder_def using sup_inf_singl(1)
moreover
from joinLatt, assms have $$\text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \})$$ unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space(1), sup_inf_singl(2)
ultimately have $$\text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} )$$ by (rule sup_sup )
moreover
have $$\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \} = \{\text{sup}\{x,y\}, \text{sup}\{z\}\}$$ and $$\bigcup \mathcal{T} = \{x,y,z\}$$
ultimately show $$(\text{sup}\{x,y,z\}) = \text{sup}\{\text{sup}\{x,y\}, \text{sup}\{z\}\}$$
qed
also
from assms, joinLatt have $$.\ .\ .\ = \text{sup}\{\text{sup}\{x,y\}, z\}$$ unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props, sup_inf_singl(2)
also
from assms, joinLatt have $$.\ .\ .\ = (\text{sup}\{x,y\}) \sqcup z$$ unfolding IsJoinSemilattice_def, IsPartOrder_def using join_props
also
from joinLatt, assms(1,2) have $$.\ .\ .\ = x\sqcup y\sqcup z$$ using join_val(2)
finally show $$x\sqcup (y\sqcup z) = x\sqcup y\sqcup z$$
qed

Join is idempotent.

lemma (in join_semilatt) join_idempotent:

assumes $$x\in L$$

shows $$x\sqcup x = x$$ using joinLatt, assms, join_val(2), IsJoinSemilattice_def, IsPartOrder_def, sup_inf_singl(2)

The meet_semilatt locale is the dual of the join-semilattice locale defined above. We will use the $$\sqcap$$ symbol to denote join, giving it ab bit higher precedence.

Locale meet_semilatt

assumes meetLatt: $$\text{IsMeetSemilattice}(L,r)$$

defines $$x \sqcap y \equiv \text{Meet}(L,r)\langle x,y\rangle$$

defines $$\text{inf}A \equiv \text{Infimum}(r,A)$$

Meet of the elements of the lattice is in the lattice.

lemma (in meet_semilatt) meet_props:

assumes $$x\in L$$, $$y\in L$$

shows $$x\sqcap y \in L$$ and $$x\sqcap y = \text{inf}\{x,y\}$$proof
from meetLatt, assms have $$\text{Meet}(L,r)\langle x,y\rangle \in L$$ using meet_is_binop, apply_funtype
thus $$x\sqcap y \in L$$
from meetLatt, assms have $$\text{Meet}(L,r)\langle x,y\rangle = \text{Infimum}(r,\{x,y\})$$ using meet_val(2)
thus $$x\sqcap y = \text{inf}\{x,y\}$$
qed

Meet is associative.

lemma (in meet_semilatt) meet_assoc:

assumes $$x\in L$$, $$y\in L$$, $$z\in L$$

shows $$x\sqcap (y\sqcap z) = x\sqcap y\sqcap z$$proof
from meetLatt, assms(2,3) have $$x\sqcap (y\sqcap z) = x\sqcap (\text{inf}\{y,z\})$$ using meet_val
also
from assms, meetLatt have $$.\ .\ .\ = \text{inf}\{\text{inf}\{x\}, \text{inf}\{y,z\}\}$$ unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props, sup_inf_singl(4)
also
have $$.\ .\ .\ = \text{inf}\{x,y,z\}$$proof
let $$\mathcal{T} = \{\{x\},\{y,z\}\}$$
from meetLatt have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$ unfolding IsMeetSemilattice_def, IsPartOrder_def
moreover
from meetLatt, assms have $$\forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T)$$ unfolding IsMeetSemilattice_def, IsPartOrder_def using sup_inf_singl(3)
moreover
from meetLatt, assms have $$\text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \})$$ unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space(1), sup_inf_singl(4)
ultimately have $$\text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} )$$ by (rule inf_inf )
moreover
have $$\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \} = \{\text{inf}\{x\}, \text{inf}\{y,z\}\}$$ and $$\bigcup \mathcal{T} = \{x,y,z\}$$
ultimately show $$(\text{inf}\{\text{inf}\{x\}, \text{inf}\{y,z\}\}) = \text{inf}\{x,y,z\}$$
qed
also
have $$.\ .\ .\ = \text{inf}\{\text{inf}\{x,y\}, \text{inf}\{z\}\}$$proof
let $$\mathcal{T} = \{\{x,y\},\{z\}\}$$
from meetLatt have $$r \subseteq L\times L$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$ unfolding IsMeetSemilattice_def, IsPartOrder_def
moreover
from meetLatt, assms have $$\forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T)$$ unfolding IsMeetSemilattice_def, IsPartOrder_def using sup_inf_singl(3)
moreover
from meetLatt, assms have $$\text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \})$$ unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space(1), sup_inf_singl(4)
ultimately have $$\text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} )$$ by (rule inf_inf )
moreover
have $$\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \} = \{\text{inf}\{x,y\}, \text{inf}\{z\}\}$$ and $$\bigcup \mathcal{T} = \{x,y,z\}$$
ultimately show $$(\text{inf}\{x,y,z\}) = \text{inf}\{\text{inf}\{x,y\}, \text{inf}\{z\}\}$$
qed
also
from assms, meetLatt have $$.\ .\ .\ = \text{inf}\{\text{inf}\{x,y\}, z\}$$ unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props, sup_inf_singl(4)
also
from assms, meetLatt have $$.\ .\ .\ = (\text{inf}\{x,y\}) \sqcap z$$ unfolding IsMeetSemilattice_def, IsPartOrder_def using meet_props
also
from meetLatt, assms(1,2) have $$.\ .\ .\ = x\sqcap y\sqcap z$$ using meet_val
finally show $$x\sqcap (y\sqcap z) = x\sqcap y\sqcap z$$
qed

Meet is idempotent.

lemma (in meet_semilatt) meet_idempotent:

assumes $$x\in L$$

shows $$x\sqcap x = x$$ using meetLatt, assms, meet_val, IsMeetSemilattice_def, IsPartOrder_def, sup_inf_singl(4)
end
lemma Order_ZF_1_L2:

assumes $$\text{IsLinOrder}(X,r)$$

shows $$\text{IsPartOrder}(X,r)$$
Definition of IsLinOrder: $$\text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X)$$
Definition of IsMeetSemilattice: $$\text{IsMeetSemilattice}(L,r) \equiv$$ $$r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAnInfimum}(r,\{x,y\}))$$
lemma inf_sup_two_el:

assumes $$\text{antisym}(r)$$, $$r \text{ is total on } X$$, $$x\in X$$, $$y\in X$$

shows $$\text{HasAnInfimum}(r,\{x,y\})$$, $$\text{Minimum}(r,\{x,y\}) = \text{Infimum}(r,\{x,y\})$$, $$\text{HasAsupremum}(r,\{x,y\})$$, $$\text{Maximum}(r,\{x,y\}) = \text{Supremum}(r,\{x,y\})$$
Definition of IsJoinSemilattice: $$\text{IsJoinSemilattice}(L,r) \equiv$$ $$r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \text{HasAsupremum}(r,\{x,y\}))$$
lemma inf_sup_two_el:

assumes $$\text{antisym}(r)$$, $$r \text{ is total on } X$$, $$x\in X$$, $$y\in X$$

shows $$\text{HasAnInfimum}(r,\{x,y\})$$, $$\text{Minimum}(r,\{x,y\}) = \text{Infimum}(r,\{x,y\})$$, $$\text{HasAsupremum}(r,\{x,y\})$$, $$\text{Maximum}(r,\{x,y\}) = \text{Supremum}(r,\{x,y\})$$
Definition of IsAlattice: $$r \text{ is a lattice on } L \equiv \text{IsJoinSemilattice}(L,r) \wedge \text{IsMeetSemilattice}(L,r)$$
Definition of IsPartOrder: $$\text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r)$$
Definition of HasAsupremum: $$\text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\})$$
lemma sup_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAminimum}(r,\bigcap a\in A.\ r\{a\})$$

shows $$\text{Supremum}(r,A) \in X$$ and $$\forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r$$
Definition of Join: $$\text{Join}(L,r) \equiv \{\langle p, \text{Supremum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\}$$
lemma ZF_fun_from_total:

assumes $$\forall x\in X.\ b(x) \in Y$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
lemma join_is_binop:

assumes $$\text{IsJoinSemilattice}(L,r)$$

shows $$\text{Join}(L,r) : L\times L \rightarrow L$$
lemma ZF_fun_from_tot_val:

assumes $$f:X\rightarrow Y$$, $$x\in X$$ and $$f = \{\langle x,b(x)\rangle .\ x\in X\}$$

shows $$f(x) = b(x)$$ and $$b(x)\in Y$$
lemma sup_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAminimum}(r,\bigcap a\in A.\ r\{a\})$$

shows $$\text{Supremum}(r,A) \in X$$ and $$\forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r$$
Definition of HasAnInfimum: $$\text{HasAnInfimum}(r,A) \equiv \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\})$$
lemma inf_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\})$$

shows $$\text{Infimum}(r,A) \in X$$ and $$\forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r$$
Definition of Meet: $$\text{Meet}(L,r) \equiv \{\langle p, \text{Infimum}(r,\{\text{fst}(p),\text{snd}(p)\})\rangle .\ p \in L\times L\}$$
lemma meet_is_binop:

assumes $$\text{IsMeetSemilattice}(L,r)$$

shows $$\text{Meet}(L,r) : L\times L \rightarrow L$$
lemma inf_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\})$$

shows $$\text{Infimum}(r,A) \in X$$ and $$\forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r$$
lemma meet_val:

assumes $$\text{IsMeetSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$m \equiv \text{Meet}(L,r)\langle x,y\rangle$$

shows $$m\in L$$, $$m = \text{Infimum}(r,\{x,y\})$$, $$\langle m,x\rangle \in r$$, $$\langle m,y\rangle \in r$$
Definition of DownDirects: $$r \text{ down-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle z,x\rangle \in r \wedge \langle z,y\rangle \in r)$$
lemma join_val:

assumes $$\text{IsJoinSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$j \equiv \text{Join}(L,r)\langle x,y\rangle$$

shows $$j\in L$$, $$j = \text{Supremum}(r,\{x,y\})$$, $$\langle x,j\rangle \in r$$, $$\langle y,j\rangle \in r$$
Definition of UpDirects: $$r \text{ up-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r)$$
lemma join_val:

assumes $$\text{IsJoinSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$j \equiv \text{Join}(L,r)\langle x,y\rangle$$

shows $$j\in L$$, $$j = \text{Supremum}(r,\{x,y\})$$, $$\langle x,j\rangle \in r$$, $$\langle y,j\rangle \in r$$
lemma (in join_semilatt) join_props:

assumes $$x\in L$$, $$y\in L$$

shows $$x\sqcup y \in L$$ and $$x\sqcup y = \text{sup}\{x,y\}$$
lemma sup_inf_singl:

assumes $$\text{antisym}(r)$$, $$\text{refl}(X,r)$$, $$z\in X$$

shows $$\text{HasAsupremum}(r,\{z\})$$, $$\text{Supremum}(r,\{z\}) = z$$ and $$\text{HasAnInfimum}(r,\{z\})$$, $$\text{Infimum}(r,\{z\}) = z$$
lemma sup_inf_singl:

assumes $$\text{antisym}(r)$$, $$\text{refl}(X,r)$$, $$z\in X$$

shows $$\text{HasAsupremum}(r,\{z\})$$, $$\text{Supremum}(r,\{z\}) = z$$ and $$\text{HasAnInfimum}(r,\{z\})$$, $$\text{Infimum}(r,\{z\}) = z$$
lemma sup_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAminimum}(r,\bigcap a\in A.\ r\{a\})$$

shows $$\text{Supremum}(r,A) \in X$$ and $$\forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r$$
lemma sup_sup:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$, $$\forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T)$$, $$\text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \})$$

shows $$\text{HasAsupremum}(r,\bigcup \mathcal{T} )$$ and $$\text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} )$$
lemma meet_val:

assumes $$\text{IsMeetSemilattice}(L,r)$$, $$x\in L$$, $$y\in L$$

defines $$m \equiv \text{Meet}(L,r)\langle x,y\rangle$$

shows $$m\in L$$, $$m = \text{Infimum}(r,\{x,y\})$$, $$\langle m,x\rangle \in r$$, $$\langle m,y\rangle \in r$$
lemma (in meet_semilatt) meet_props:

assumes $$x\in L$$, $$y\in L$$

shows $$x\sqcap y \in L$$ and $$x\sqcap y = \text{inf}\{x,y\}$$
lemma sup_inf_singl:

assumes $$\text{antisym}(r)$$, $$\text{refl}(X,r)$$, $$z\in X$$

shows $$\text{HasAsupremum}(r,\{z\})$$, $$\text{Supremum}(r,\{z\}) = z$$ and $$\text{HasAnInfimum}(r,\{z\})$$, $$\text{Infimum}(r,\{z\}) = z$$
lemma sup_inf_singl:

assumes $$\text{antisym}(r)$$, $$\text{refl}(X,r)$$, $$z\in X$$

shows $$\text{HasAsupremum}(r,\{z\})$$, $$\text{Supremum}(r,\{z\}) = z$$ and $$\text{HasAnInfimum}(r,\{z\})$$, $$\text{Infimum}(r,\{z\}) = z$$
lemma inf_in_space:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\})$$

shows $$\text{Infimum}(r,A) \in X$$ and $$\forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r$$
lemma inf_inf:

assumes $$r \subseteq X\times X$$, $$\text{antisym}(r)$$, $$\text{trans}(r)$$, $$\forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T)$$, $$\text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \})$$

shows $$\text{HasAnInfimum}(r,\bigcup \mathcal{T} )$$ and $$\text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} )$$