Theorems · Definition · order theory

WellQuasiOrdered

{α : Type u_1} → (α → α → Prop) → Prop

A well quasi-order or WQO is a relation such that any infinite sequence contains an infinite monotonic subsequence, or equivalently, two elements f m and f n with m < n and r (f m) (f n). For a preorder, this is equivalent to having a well-founded order with no infinite antichains. Despite the nomenclature, we don't require the relation to be preordered. Moreover, a well quasi-order will not in general be a well-order.

Defined in

Mathlib.Order.WellQuasiOrder

Cited by

15 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms