Order, lattices, ordered algebraic structures Definition

Successor order

Builds on Partial order Successor function

Definition

Let $(P, \le)$ be a partially ordered set, and write $a < b$ when $a \le b$ and $a \ne b$ . A successor order on $P$ is a map $\operatorname{succ} \colon P \to P$ such that:

$a \le \operatorname{succ}(a)$ for all $a \in P$ .
If $\operatorname{succ}(a) \le a$ , then $a$ is a maximal element of $P$ .
If $a < b$ , then $\operatorname{succ}(a) \le b$ .

Remarks

When $a$ is not maximal, the clauses say that $\operatorname{succ}(a)$ is the least element of $\set{b \in P : a < b}$ ; when $a$ is maximal, $\operatorname{succ}(a) = a$ . So the map, if it exists, is unique.

Example: $\Z$ with $\operatorname{succ}(n) = n + 1$ . Check: $n \le n + 1$ ; the inequality $n + 1 \le n$ never holds, so clause 2 is empty; and $n < m$ for integers means $n + 1 \le m$ . On $\N$ this is the successor function.

Non-example: $\Q$ with the usual order has no successor order. No rational is maximal, so clauses 1 and 2 force $a < \operatorname{succ}(a)$ ; then $b = (a + \operatorname{succ}(a))/2$ satisfies $a < b < \operatorname{succ}(a)$ , which breaks clause 3.

The dual notion is a predecessor order. In Mathlib this is the class SuccOrder.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Partial order concept
Successor function concept
Successor order definition

Tag	`Z7RGVW5EWN`
URI	`m2://Z7RGVW5EWN`
Kind	definition
Writing	W0 stub
MSC	06A06, 06A05
Defines	Successor order
Uses	Partial order, Successor function

Successor order

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here