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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
\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}
|
