diff options
Diffstat (limited to 'library/order')
| -rw-r--r-- | library/order/order.tex | 102 | ||||
| -rw-r--r-- | library/order/quasiorder.tex | 51 | ||||
| -rw-r--r-- | library/order/semilattice.tex | 41 |
3 files changed, 194 insertions, 0 deletions
diff --git a/library/order/order.tex b/library/order/order.tex new file mode 100644 index 0000000..339bad8 --- /dev/null +++ b/library/order/order.tex @@ -0,0 +1,102 @@ +\import{relation.tex} +\import{relation/properties.tex} +\import{order/quasiorder.tex} + +% also called "(partial) ordering" or "partial order" to contrast with connex (i.e. "total") orders. +\begin{abbreviation}\label{order} + $R$ is an order iff + $R$ is an antisymmetric quasiorder. +\end{abbreviation} + +\begin{abbreviation}\label{order_on} + $R$ is an order on $A$ iff + $R$ is an antisymmetric quasiorder on $A$. +\end{abbreviation} + +\begin{abbreviation}\label{strictorder} + $R$ is a strict order iff + $R$ is transitive and asymmetric. +\end{abbreviation} + +\begin{struct}\label{orderedset} + An ordered set $X$ is a quasiordered set + such that + \begin{enumerate} + \item\label{orderedset_antisym} $\lt[X]$ is antisymmetric. + \end{enumerate} +\end{struct} + +\begin{definition}\label{tostrictorder} + $\tostrictorder{R} = \{w\in R\mid \fst{w}\neq\snd{w}\}$. +\end{definition} + +\begin{definition}\label{toorder} + $\toorder{A}{R} = R\union\identity{A}$. +\end{definition} + +\begin{proposition}\label{tostrictorder_iff} + $(a,b)\in\tostrictorder{R}$ iff $(a,b)\in R$ and $a\neq b$. +\end{proposition} +\begin{proof} + Follows by \cref{tostrictorder,fst_eq,snd_eq}. +\end{proof} + +\begin{proposition}\label{toorder_reflexive} + $\toorder{A}{R}$ is reflexive on $A$. +\end{proposition} + +\begin{proposition}\label{toorder_intro} + Suppose $(a,b)\in R$. + Then $(a,b)\in\toorder{A}{R}$. +\end{proposition} +\begin{proof} + $R\subseteq\toorder{A}{R}$. +\end{proof} + +\begin{proposition}\label{toorder_elim} + Suppose $(a,b)\in\toorder{A}{R}$. + Then $(a,b)\in R$ or $a = b$. +\end{proposition} +\begin{proof} + Follows by \cref{toorder,id,union_iff,upair_intro_right,tostrictorder_iff}. +\end{proof} + +\begin{proposition}\label{toorder_iff} + $(a,b)\in\toorder{A}{R}$ iff $(a,b)\in R$ or $a = b\in A$. +\end{proposition} + +\begin{proposition}\label{strictorder_from_order} + Suppose $R$ is an order. + Then $\tostrictorder{R}$ is a strict order. +\end{proposition} +\begin{proof} + $\tostrictorder{R}$ is asymmetric. + $\tostrictorder{R}$ is transitive. +\end{proof} + +\begin{proposition}\label{order_from_strictorder} + Suppose $R$ is a strict order. + Suppose $R$ is a binary relation on $A$. + Then $\toorder{A}{R}$ is an order on $A$. +\end{proposition} +\begin{proof} + $\toorder{A}{R}$ is antisymmetric. + $\toorder{A}{R}$ is transitive by \cref{transitive,toorder_iff}. + $\toorder{A}{R}$ is reflexive on $A$. +\end{proof} + +\begin{proposition}\label{subseteqrel_antisymmetric} + $\subseteqrel{A}$ is antisymmetric. +\end{proposition} +\begin{proof} + Follows by \cref{subseteqrel,antisymmetric,pair_eq_iff,subseteq_antisymmetric}. +\end{proof} + + +\begin{proposition}\label{subseteqrel_is_order} + $\subseteqrel{A}$ is an order on $A$. +\end{proposition} +\begin{proof} + $\subseteqrel{A}$ is a quasiorder on $A$ by \cref{subseteqrel_is_quasiorder}. + $\subseteqrel{A}$ is antisymmetric by \cref{subseteqrel_antisymmetric}. +\end{proof} diff --git a/library/order/quasiorder.tex b/library/order/quasiorder.tex new file mode 100644 index 0000000..ab325e7 --- /dev/null +++ b/library/order/quasiorder.tex @@ -0,0 +1,51 @@ +\import{relation.tex} +\import{relation/properties.tex} + +\subsection{Quasiorders} + +% also called preorder +\begin{abbreviation}\label{quasiorder} + $R$ is a quasiorder iff + $R$ is quasireflexive and transitive. +\end{abbreviation} + +% also called preorder +\begin{abbreviation}\label{quasiorder_on} + $R$ is a quasiorder on $A$ iff + $R$ is a binary relation on $A$ and + $R$ is reflexive on $A$ and transitive. +\end{abbreviation} + +\begin{struct}\label{quasiordered_set} + A quasiordered set $X$ is a onesorted structure + equipped with + \begin{enumerate} + \item $\lt$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{quasiorder_type} $\lt[X]$ is a binary relation on $\carrier[X]$. + \item\label{quasiorder_refl} $\lt[X]$ is reflexive on $\carrier[X]$. + \item\label{quasiorder_tran} $\lt[X]$ is transitive. + \end{enumerate} +\end{struct} + +\begin{lemma}\label{quasiorder_transitive_double} + Let $X$ be a quasiordered set. + Let $a, b, c, d \in X$. + Suppose $a\mathrel{\lt[X]} b\mathrel{\lt[X]} c\mathrel{\lt[X]} d$. + Then $a\mathrel{\lt[X]} d$. +\end{lemma} +\begin{proof} + $\lt[X]$ is transitive. + Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. + Hence $a\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. +\end{proof} + +\begin{proposition}\label{subseteqrel_is_quasiorder} + $\subseteqrel{A}$ is a quasiorder on $A$. +\end{proposition} +\begin{proof} + $\subseteqrel{A}$ is reflexive on $A$. + $\subseteqrel{A}$ is transitive. +\end{proof} diff --git a/library/order/semilattice.tex b/library/order/semilattice.tex new file mode 100644 index 0000000..51af68b --- /dev/null +++ b/library/order/semilattice.tex @@ -0,0 +1,41 @@ +\import{order/partial-order.tex} + +\begin{struct}\label{meet_semilattice} + A meet semilattice $X$ is a partial order + equipped with + \begin{enumerate} + \item $\meet$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{meet_type} for all $x,y\in \carrier[X]$ we have + $\meet[X](x,y)\in 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 + $a\mathrel{\lt[X]} \meet[X](x,y)$. + \end{enumerate} +\end{struct} + + +\begin{proposition}\label{meet_idempotent} + Let $X$ be a meet semilattice. + Then $\meet(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)$. +\end{proof} + +%\begin{proposition}\label{meet_comm} +% Let $X$ be a meet semilattice. +% Suppose $x, y\in X$. +% Then $\meet(x,y) = \meet(y,x)$. +%\end{proposition} + +%\begin{proposition}\label{meet_assoc} +% Let $X$ be a meet semilattice. +% Suppose $x, y, z\in X$. +% Then $\meet(x,\meet(y,z)) = \meet(\meet(x,y),z)$. +%\end{proposition} |