1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
\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{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}
|
