Order, lattices, ordered algebraic structures Definition

Partially well-ordered set

Builds on Partial order Sequence Well-quasi-ordering

Definition

Let $(P, \le)$ be a partially ordered set. The set $P$ is partially well-ordered when for every infinite sequence $x_1, x_2, x_3, \ldots$ in $P$ there are indices $i < j$ with $x_i \le x_j$ . More generally, let $S$ be a subset of a preordered set $(X, \le)$ . The subset $S$ is partially well-ordered when every infinite sequence in $S$ has indices $i < j$ with $x_i \le x_j$ .

Remarks

So a partially well-ordered set is a partial order that is a well-quasi-ordering.

Example: $\N^2$ with the product order. Check: from any sequence $(a_n, b_n)$ extract a subsequence on which $a_n$ is non-decreasing, then a further subsequence on which $b_n$ is non-decreasing; two terms of it give $i < j$ with $x_i \le x_j$ .

Non-example: $\N$ with the trivial order, where $x \le y$ only when $x = y$ , is a partial order but not partially well-ordered: the sequence $0, 1, 2, \ldots$ has no $i < j$ with $x_i \le x_j$ .

Every well-ordered set is partially well-ordered. In Mathlib the subset form is Set.IsPWO.

Reading path

To understand this page from the ground up, read these 4 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

Tag	`ZV239N9H5B`
URI	`m2://ZV239N9H5B`
Kind	definition
Writing	W0 stub
MSC	06A06, 06A07
Defines	Partially well-ordered set
Uses	Partial order, Sequence, Well-quasi-ordering

Partially well-ordered set

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here