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\})) \)
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\} \)
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
Join of \(x,y\) is less or equal than any upper bound for \(\{ x,y\}\).
lemma join_least_upbound:
assumes \( \text{IsJoinSemilattice}(L,r) \), \( \langle x,z\rangle \in r \), \( \langle y,z\rangle \in r \)
shows \( \langle \text{Join}(L,r)\langle x,y\rangle ,z\rangle \in r \)proof from assms have \( x\in L \), \( y\in L \) unfolding IsJoinSemilattice_def
with assms show \( thesis \) using join_val, sup_leq_up_bnd unfolding IsJoinSemilattice_def, IsPartOrder_def
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 join semilattice a union of two sets that have suprema has a supremum.
lemma join_semilat_sup_two:
assumes \( \text{IsJoinSemilattice}(L,r) \), \( \text{HasAsupremum}(r,A) \), \( \text{HasAsupremum}(r,B) \)
shows \( \text{HasAsupremum}(r,A\cup B) \) and \( \text{Supremum}(r,A\cup B) = \text{Join}(L,r)\langle \text{Supremum}(r,A), \text{Supremum}(r,B)\rangle \)proof let \( S_A = \text{Supremum}(r,A) \)
let \( S_B = \text{Supremum}(r,B) \)
from assms have \( S_A\in L \), \( S_B\in L \) unfolding IsJoinSemilattice_def, IsPartOrder_def, HasAsupremum_def using sup_in_space
with assms have I: \( \text{Join}(L,r)\langle S_A,S_B\rangle = \text{Supremum}(r,\{S_A,S_B\}) \) and II: \( r\subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \{A,B\}.\ \text{HasAsupremum}(r,T) \), \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \{A,B\}\}) \) using join_val(2) unfolding IsJoinSemilattice_def, IsPartOrder_def
from II have \( \text{HasAsupremum}(r,\bigcup \{A,B\}) \) by (rule sup_sup )
from II have \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \{A,B\}\}) = \text{Supremum}(r,\bigcup \{A,B\}) \) by (rule sup_sup )
with \( \text{HasAsupremum}(r,\bigcup \{A,B\}) \), I show \( \text{HasAsupremum}(r,A\cup B) \) and \( \text{Supremum}(r,A\cup B) = \text{Join}(L,r)\langle S_A,S_B\rangle \)
qed
In a meet semilattice a union of two sets that have infima has an infimum.
lemma meet_semilat_inf_two:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( \text{HasAnInfimum}(r,A) \), \( \text{HasAnInfimum}(r,B) \)
shows \( \text{HasAnInfimum}(r,A\cup B) \) and \( \text{Infimum}(r,A\cup B) = \text{Meet}(L,r)\langle \text{Infimum}(r,A), \text{Infimum}(r,B)\rangle \)proof let \( I_A = \text{Infimum}(r,A) \)
let \( I_B = \text{Infimum}(r,B) \)
from assms have \( I_A\in L \), \( I_B\in L \) unfolding IsMeetSemilattice_def, IsPartOrder_def, HasAnInfimum_def using inf_in_space
with assms have I: \( \text{Meet}(L,r)\langle I_A,I_B\rangle = \text{Infimum}(r,\{I_A,I_B\}) \) and II: \( r\subseteq L\times L \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \{A,B\}.\ \text{HasAnInfimum}(r,T) \), \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \{A,B\}\}) \) using meet_val(2) unfolding IsMeetSemilattice_def, IsPartOrder_def
from II have \( \text{HasAnInfimum}(r,\bigcup \{A,B\}) \) by (rule inf_inf )
from II have \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \{A,B\}\}) = \text{Infimum}(r,\bigcup \{A,B\}) \) by (rule inf_inf )
with \( \text{HasAnInfimum}(r,\bigcup \{A,B\}) \), I show \( \text{HasAnInfimum}(r,A\cup B) \) and \( \text{Infimum}(r,A\cup B) = \text{Meet}(L,r)\langle I_A,I_B\rangle \)
qed
In a join semilattice every nonempty finite set has a supremum.
lemma join_semilat_fin_sup:
assumes \( \text{IsJoinSemilattice}(L,r) \), \( N\in \text{FinPow}(L) \), \( N\neq \emptyset \)
shows \( \text{HasAsupremum}(r,N) \)proof let \( C = \{B\in Pow(L).\ \text{HasAsupremum}(r,B)\} \)
from assms(1,2) have \( \forall x\in N.\ \{x\}\in C \) unfolding IsJoinSemilattice_def, IsPartOrder_def, FinPow_def using sup_inf_singl(1)
from assms(1) have \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) using join_semilat_sup_two
with assms(2,3), \( \forall x\in N.\ \{x\}\in C \) have \( N\in C \) by (rule union_two_union_fin_nempty )
thus \( \text{HasAsupremum}(r,N) \)
qed
In a meet semilattice every nonempty finite set has a infimum.
lemma meet_semilat_fin_inf:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( N\in \text{FinPow}(L) \), \( N\neq \emptyset \)
shows \( \text{HasAnInfimum}(r,N) \)proof let \( C = \{B\in Pow(L).\ \text{HasAnInfimum}(r,B)\} \)
from assms(1,2) have \( \forall x\in N.\ \{x\}\in C \) unfolding IsMeetSemilattice_def, IsPartOrder_def, FinPow_def using sup_inf_singl(3)
from assms(1) have \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) using meet_semilat_inf_two
with assms(2,3), \( \forall x\in N.\ \{x\}\in C \) have \( N\in C \) by (rule union_two_union_fin_nempty )
thus \( \text{HasAnInfimum}(r,N) \)
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
qed
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
also 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
qed
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\} \)
have \( .\ .\ .\ = \text{sup}\{\text{sup}\{x,y\}, \text{sup}\{z\}\} \)proof
also 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
qed
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\}\} \)
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 \)
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
qed
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
also 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
qed
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\} \)
have \( .\ .\ .\ = \text{inf}\{\text{inf}\{x,y\}, \text{inf}\{z\}\} \)proof
also 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
qed
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\}\} \)
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 \)
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)Lattices
Here we study lattices, i.e. structures where both meet and join are defined.
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) \)
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
qed
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
Complete lattices
The definition of a lattice requires that every two-element set has a supremum and infimum. As we show in join_semilat_fin_sup and meet_semilat_fin_inf this implies that every finite subset of the lattice has supremum and infimum. In this section we study structures in which every nonempty subset (not necessarily finite) has both supremum and infimum.
Wikipedia defines a complete lattice as a partially ordered set in which every subset has both supremum and infimum. The way we define supremum and infimum only nonempty sets can have infima or suprema so to avoid inconsistency we define a complete lattice as the one in which all nonempty subsets have both infima and suprema. We also add the assumption that the carrier is nonempty so that we don't have to repeat that assumption in every proposition about complete lattices.
definition
\( \text{IsCompleteLattice}(L,r) \equiv L\neq \emptyset \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge \) \( (\forall A\in Pow(L)\setminus \{\emptyset \}.\ ( \text{HasAsupremum}(r,A) \wedge \text{HasAnInfimum}(r,A))) \)
Complete lattices are bounded and have both maximum and minimum.
lemma compl_lat_bounded:
assumes \( \text{IsCompleteLattice}(L,r) \)
shows \( \text{HasAmaximum}(r,L) \), \( \text{HasAminimum}(r,L) \), \( \text{IsBounded}(L,r) \)proof from assms have \( \text{Supremum}(r,L)\in L \) and \( \text{Infimum}(r,L)\in L \) using sup_in_space(1), inf_in_space(1) unfolding IsCompleteLattice_def, IsPartOrder_def, HasAsupremum_def, HasAnInfimum_def
with assms show \( \text{HasAmaximum}(r,L) \), \( \text{HasAminimum}(r,L) \), \( \text{IsBounded}(L,r) \) using sup_is_max(1), inf_is_min(1), Order_ZF_4_L7, Order_ZF_4_L8A unfolding IsCompleteLattice_def, IsPartOrder_def, IsBounded_def
qed
end
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\})) \)
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 \) 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 sup_leq_up_bnd:
assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)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\})) \)
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 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 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 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} ) \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
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 join_semilat_sup_two:
assumes \( \text{IsJoinSemilattice}(L,r) \), \( \text{HasAsupremum}(r,A) \), \( \text{HasAsupremum}(r,B) \)
shows \( \text{HasAsupremum}(r,A\cup B) \) and \( \text{Supremum}(r,A\cup B) = \text{Join}(L,r)\langle \text{Supremum}(r,A), \text{Supremum}(r,B)\rangle \) lemma union_two_union_fin_nempty:
assumes \( N\in \text{FinPow}(X) \), \( N\neq \emptyset \), \( \forall x\in N.\ \{x\} \in C \), \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \)
shows \( N\in C \) 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 meet_semilat_inf_two:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( \text{HasAnInfimum}(r,A) \), \( \text{HasAnInfimum}(r,B) \)
shows \( \text{HasAnInfimum}(r,A\cup B) \) and \( \text{Infimum}(r,A\cup B) = \text{Meet}(L,r)\langle \text{Infimum}(r,A), \text{Infimum}(r,B)\rangle \) 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) \)
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 (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_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 (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 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 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) \)
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\}) \) 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 IsCompleteLattice:
\( \text{IsCompleteLattice}(L,r) \equiv L\neq \emptyset \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge \)
\( (\forall A\in Pow(L)\setminus \{\emptyset \}.\ ( \text{HasAsupremum}(r,A) \wedge \text{HasAnInfimum}(r,A))) \)
lemma sup_is_max:
assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \text{Supremum}(r,A) \in A \)
shows \( \text{HasAmaximum}(r,A) \) and \( \text{Maximum}(r,A) = \text{Supremum}(r,A) \) lemma inf_is_min:
assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( \text{Infimum}(r,A) \in A \)
shows \( \text{HasAminimum}(r,A) \) and \( \text{Minimum}(r,A) = \text{Infimum}(r,A) \) lemma Order_ZF_4_L7:
assumes \( \text{HasAmaximum}(r,A) \)
shows \( \text{IsBoundedAbove}(A,r) \) lemma Order_ZF_4_L8A:
assumes \( \text{HasAminimum}(r,A) \)
shows \( \text{IsBoundedBelow}(A,r) \)Definition of IsBounded:
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8