diff options
Diffstat (limited to 'library/order/semilattice.tex')
| -rw-r--r-- | library/order/semilattice.tex | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/library/order/semilattice.tex b/library/order/semilattice.tex index 51af68b..76bbe56 100644 --- a/library/order/semilattice.tex +++ b/library/order/semilattice.tex @@ -1,7 +1,8 @@ -\import{order/partial-order.tex} +\import{order/order.tex} +\import{function.tex} \begin{struct}\label{meet_semilattice} - A meet semilattice $X$ is a partial order + A meet semilattice $X$ is an ordered set equipped with \begin{enumerate} \item $\meet$ @@ -9,7 +10,7 @@ such that \begin{enumerate} \item\label{meet_type} for all $x,y\in \carrier[X]$ we have - $\meet[X](x,y)\in X$. + $\meet[X](x,y)\in \carrier[X]$. \item\label{meet_lb} for all $x,y\in \carrier[X]$ we have $\meet[X](x,y) \mathrel{\lt[X]} x, y$. \item\label{meet_glb} for all $a,x,y\in \carrier[X]$ such that $a\mathrel{\lt[X]} x, y$ we have @@ -20,12 +21,16 @@ \begin{proposition}\label{meet_idempotent} Let $X$ be a meet semilattice. - Then $\meet(x,x) = x$. + Let $x\in\carrier[X]$. + Then $\meet[X](x,x) = x$. \end{proposition} \begin{proof} - $\meet(x,x) \mathrel{\lt} x$. - $x\mathrel{\lt[X]} x, x$. - Thus $x\mathrel{\lt[X]} \meet(x,x)$. + We have $\meet[X](x,x)\in\carrier[X]$ by \cref{meet_type}. + We have $\meet[X](x,x)\mathrel{\lt[X]}x$ by \cref{meet_lb}. + We have $x\mathrel{\lt[X]}x$ + by \cref{meet_semilattice,orderedset,quasiorder_refl,reflexive_on}. + Thus $x\mathrel{\lt[X]}\meet[X](x,x)$ by \cref{meet_glb}. + Follows by \cref{meet_semilattice,orderedset,orderedset_antisym,antisymmetric}. \end{proof} %\begin{proposition}\label{meet_comm} |