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
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
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
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) 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} ) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8