\import{relation.tex}
\import{relation/properties.tex}
\import{order/quasiorder.tex}
\section{Order}

% 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{proof}
    Follows by \cref{toorder,reflexive_on,id_iff,union_iff}.
\end{proof}

\begin{proposition}\label{toorder_intro}
    Suppose $(a,b)\in R$.
    Then $(a,b)\in\toorder{A}{R}$.
\end{proposition}
\begin{proof}
    Follows by \cref{toorder,union_iff}.
\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{proof}
    Follows by \cref{toorder,id_iff,union_iff}.
\end{proof}

\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
        by \cref{antisymmetric,asymmetric,tostrictorder_iff}.
    Show for all $a,b,c$ such that
        $a\mathrel{\tostrictorder{R}}b$ and
        $b\mathrel{\tostrictorder{R}}c$
        we have $a\mathrel{\tostrictorder{R}}c$.
    \begin{subproof}
        Fix $a,b,c$.
        Assume $a\mathrel{\tostrictorder{R}}b$ and
            $b\mathrel{\tostrictorder{R}}c$.
        We have $a\mathrel{R}b$ and $b\mathrel{R}c$
            by \cref{tostrictorder_iff}.
        Thus $a\mathrel{R}c$ by \cref{transitive}.
        We have $a\neq c$ by \cref{asymmetric}.
        Follows by \cref{tostrictorder_iff}.
    \end{subproof}
    Thus $\tostrictorder{R}$ is transitive by \cref{transitive}.
    Follows by assumption.
\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}
    $\identity{A}\subseteq A\times A$
        by \cref{id_elem_rels,rels_elim}.
    Thus $\toorder{A}{R}\subseteq A\times A$
        by \cref{toorder,union_subsets_is_subset}.
    Hence $\toorder{A}{R}$ is a binary relation on $A$
        by assumption.
    $\toorder{A}{R}$ is antisymmetric
        by \cref{antisymmetric,asymmetric,toorder_iff}.
    $\toorder{A}{R}$ is transitive by \cref{transitive,toorder_iff}.
    $\toorder{A}{R}$ is reflexive on $A$ by \cref{toorder_reflexive}.
    Follows by assumption.
\end{proof}

\begin{proposition}\label{subseteqrel_antisymmetric}
    $\subseteqrel{A}$ is antisymmetric.
\end{proposition}
\begin{proof}
    Show for all $a,b$ such that
        $a\mathrel{\subseteqrel{A}}b$ and
        $b\mathrel{\subseteqrel{A}}a$
        we have $a=b$.
    \begin{subproof}
        Fix $a,b$.
        Assume $a\mathrel{\subseteqrel{A}}b$ and
            $b\mathrel{\subseteqrel{A}}a$.
        Take $x,y$ such that $(a,b)=(x,y)$ and
            $x,y\in A$ and $x\subseteq y$ by \cref{subseteqrel}.
        Then $a=x$ and $b=y$ by \cref{pair_eq_iff}.
        Thus $a\subseteq b$ by assumption.
        Take $u,v$ such that $(b,a)=(u,v)$ and
            $u,v\in A$ and $u\subseteq v$ by \cref{subseteqrel}.
        Then $b=u$ and $a=v$ by \cref{pair_eq_iff}.
        Thus $b\subseteq a$ by assumption.
        Follows by \cref{subseteq_antisymmetric}.
    \end{subproof}
    Follows by \cref{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}.
    Follows by assumption.
\end{proof}