Well quasi-orders

A well quasi-order (WQO) is a relation such that any infinite sequence contains an infinite subsequence of related elements. For a preorder, this is equivalent to having a well-founded order with no infinite antichains.

Main definitions

• WellQuasiOrdered: a predicate for WQO unbundled relations
• WellQuasiOrderedLE: a typeclass for a bundled WQO ≤ relation

TODO

• Define Set.PartiallyWellOrderedOn and Set.IsPWO in terms of these predicates, and rename them to match.

Tags

wqo, pwo, well quasi-order, partial well order, dickson order

def WellQuasiOrdered {α : Type u_1} (r : α → α → 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.

Equations

• WellQuasiOrdered r = ∀ (f : ℕ → α), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

theorem wellQuasiOrdered_of_isEmpty {α : Type u_1} [IsEmpty α] (r : α → α → Prop) : WellQuasiOrdered r

theorem IsAntichain.finite_of_wellQuasiOrdered {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) (hr : WellQuasiOrdered r) : s.Finite

theorem Finite.wellQuasiOrdered {α : Type u_1} (r : α → α → Prop) [Finite α] [IsRefl α r] : WellQuasiOrdered r

theorem WellQuasiOrdered.exists_monotone_subseq {α : Type u_1} {r : α → α → Prop} [IsPreorder α r] (h : WellQuasiOrdered r) (f : ℕ → α) : ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

theorem wellQuasiOrdered_iff_exists_monotone_subseq {α : Type u_1} {r : α → α → Prop} [IsPreorder α r] : WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

theorem WellQuasiOrdered.prod {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsPreorder α r] (hr : WellQuasiOrdered r) (hs : WellQuasiOrdered s) : WellQuasiOrdered fun (a b : α × β) => r a.1 b.1 ∧ s a.2 b.2

class WellQuasiOrderedLE (α : Type u_3) [LE α] : Prop

A typeclass for an order with a well quasi-ordered ≤ relation.

Note that this is unlike WellFoundedLT, which instead takes a < relation.

• wqo : WellQuasiOrdered fun (x1 x2 : α) => x1 ≤ x2

theorem wellQuasiOrderedLE_def (α : Type u_3) [LE α] : WellQuasiOrderedLE α ↔ WellQuasiOrdered fun (x1 x2 : α) => x1 ≤ x2

theorem wellQuasiOrdered_le {α : Type u_1} [LE α] [h : WellQuasiOrderedLE α] : WellQuasiOrdered fun (x1 x2 : α) => x1 ≤ x2

@[instance 100]

instance Finite.to_wellQuasiOrderedLE {α : Type u_1} [Preorder α] [Finite α] : WellQuasiOrderedLE α

@[instance 100]

instance WellQuasiOrderedLE.to_wellFoundedLT {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] : WellFoundedLT α

theorem WellQuasiOrdered.wellFounded {α : Type u_3} {r : α → α → Prop} [IsPreorder α r] (h : WellQuasiOrdered r) : WellFounded fun (a b : α) => r a b ∧ ¬r b a

theorem WellQuasiOrderedLE.finite_of_isAntichain {α : Type u_1} [Preorder α] [WellQuasiOrderedLE α] {s : Set α} (h : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) : s.Finite

theorem wellQuasiOrderedLE_iff {α : Type u_1} [Preorder α] : WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s → s.Finite

A preorder is well quasi-ordered iff it's well-founded and has no infinite antichains.

instance instWellQuasiOrderedLEProd {α : Type u_1} {β : Type u_2} [Preorder α] [WellQuasiOrderedLE α] [Preorder β] [WellQuasiOrderedLE β] : WellQuasiOrderedLE (α × β)

theorem wellQuasiOrderedLE_iff_wellFoundedLT {α : Type u_1} [LinearOrder α] : WellQuasiOrderedLE α ↔ WellFoundedLT α

A linear WQO is the same thing as a well-order.