## Using relations to order

We have seen some relations that convey a notion of size. On $\mathbb{R}$ (and its subsets), we have $<,\leq$. If $x < y$, then we think of $y$ as a bigger number than $x$.

For sets, subset containment $X \subseteq Y$ is similar. If $X \subseteq Y$, then every $x \in X$ is also an element of $Y$. Thus, $Y$ has more elements than $X$.

Such ordering relations can be quite useful. As such, we make two definitions.

**Definition**. Let $\prec$ be a relation on $X$. We say that $\prec$ is a *partial order* if it is

- reflexive
- antisymmetric
- and transitive. If $X$ has a partial order, we call it a
*poset*.

It is a *total order* if it is

- total
- antisymmetric
- and transistive.

In the context of partial and total orders, we will use the symbol $\prec$.

As we saw, total implies reflexive. Thus,

**Lemma**.

- Any total order is a partial order.
- A partial order that is total is a total order.

We can define partial and total orders in Lean using a structure that bundles up the three defining properties.

Our work previously lets us prove that $a \mid b$ is a partial order on $\mathbb{N}$.

It is not a total order however because | is not a total relation. For example, $2 \nmid 3$ and $3 \nmid 2$.

Other familiar examples of partial orders are:

- Sets with $\subseteq$
- $\mathbb{R}$ (or $\mathbb{Z}$ or $\mathbb{N}$) with $\leq$
- Any set with $=$ is a partial order.

Of these, only $\leq$ on $\mathbb{R}$ is a total order.

A partial order allows to ask about largest and smallest elements.

**Definition**. Let $(X, \prec)$ be a poset. A *least element* $\bot$ is an element of $X$ such that \(\forall~ x, \bot \prec x\) A *greatest element* $\top$ is an element of $X$ such that \(\forall~ x, x \prec \top\)

**Examples**.

- Let $X$ be a set. Then the poset $(\mathcal P(X),\subseteq)$ has $\varnothing$ as a least element and $X$ as a greatest element.
- The poset $(\mathbb{N},\mid)$ has $1$ as a least element and $0$ as a greatest element.

**Example**. The totally ordered set $(\mathbb{Z},\leq)$ has neither a least or a greatest element. In general, $\bot$ and $\top$ need not exist for a poset.

**Lemma**. Least elements are unique as are greatest elements.

## **Proof**. (Expand to view)

Assume we have two least elements $\bot, \bot^\prime$. Then since $\bot$ is least, we have $\bot \prec \bot^\prime$. Since $\bot'$ is least, we have $\bot^\prime \prec \bot$. From antisymmetry, we get $\bot = \bot^\prime$. An analogous argument works for uniqueness of greatest elements. ■

**Lemma**. Let $(X, \prec)$ be a poset with least element $\bot$ and greatest element $\top$. If $\bot = \top$, then $X = \lbrace \bot \rbrace$.

## **Proof**. (Expand to view)

Let $x \in X$. Then $\bot \prec x$ and $x \prec \top = \bot$. Using antisymmetry, we have $x = \bot$. ■

Suppose we have a poset $(X,\prec)$. Then we can make a new set $X_b := X \cup \lbrace -\infty \rbrace$ with a relation $\prec_b$ where \(R_{\prec_b} = R_\prec \cup \lbrace -\infty \rbrace \times X_b \subset X_b \times X_b\) is the subset of related pairs of $\prec_b$. In other words, we all the previous relations of $\prec$ hold and the new element $-\infty$ satisfies $-\infty \prec_b x$ for all $x$ (including $x = -\infty$).

Similarly, we can adjoin a greatest element $\infty$. We denate that as $X^t$.

**Lemma**. Let $(X,\prec)$ be a poset. Then $(X_b,\prec_b)$ is a poset with least element $-\infty$. Similarly, $(X^t,\prec^t)$ is a poset with greatest element $\infty$.

## **Proof**. (Expand to view)

Let's check that $(X_b,\prec_b)$ is a poset. The proof for $(X^t,\prec^t)$ is analogous so we omit it. We check reflexivity. If $x \in X$, then $x \prec_b x = x \prec x$ and we have $x \prec x$ since $\prec$ is reflexive. If $x = -\infty$, then by definition $-\infty \prec -\infty$. We check antisymmetry. Assume that $x \prec_b y$ and $y \prec_b x$. Either $x \in X$ or $x = -\infty$. If $x = \bot$, then we contradict the definition of $\prec_b$ unless $y = -\infty$ also. In the case $x,y \in X$, we know that $x = y$ from the assumed antisymmetry of $\prec$. Finally, we check transitivity. Assume that $x \prec_b y$ and $y \prec_b z$. If $z = -\infty$, then $y = -\infty$ by definition of $\prec_b$. But then $x = -\infty$ from the definition again. Thus, $x = -\infty \prec_b -\infty = z$. If $y = -\infty$, then $x = -\infty$ by definition of $\prec_b$. So $x=y \prec_b z$. If $x = -\infty$, then $x = -\infty \prec_b z$ by definition. The remaining case is where $x,y,z \in X$. But we have assumed that $\prec$ is transitive so $x = z$ in this case also. ■

**Example**. If we take $(\mathbb{R},\leq)$ as our poset then $\mathbb{R}^b_t$ is often written as $[-\infty,\infty]$.