---
tag: ZV239N9H5B
kind: definition
name: Partially well-ordered set
msc: [06A06, 06A07]
defines: H0Q4BWB23T
uses: [0QV2JS9RJ3, 0G9EKM0E15, NH25G6GC07]
sources:
  - url: https://en.wikipedia.org/wiki/Well-quasi-ordering
---

## Definition

Let $(P, \le)$ be a [[partially ordered set|0QV2JS9RJ3]].
The set $P$ is *partially well-ordered* when for every infinite [[sequence|0G9EKM0E15]] $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|NH25G6GC07]].

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`.