Well-quasi-orders: finite bases and Higman's lemma #
The finite-basis property of well-quasi-orders, that every upward-closed set is the union of
finitely many principal filters, and Higman's lemma: over a finite alphabet the sublist order on
List α is a well-quasi-order, the case of mathlib's
Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ at equality.
References #
theorem
WellQuasiOrdered.exists_finset_eq_biUnion
{α : Type u_1}
{r : α → α → Prop}
[IsPartialOrder α r]
(hr : WellQuasiOrdered r)
{s : Set α}
(hs : ∀ ⦃a b : α⦄, r a b → a ∈ s → b ∈ s)
:
∃ (F : Finset α), s = ⋃ a ∈ F, {b : α | r a b}
The finite-basis property: in a well-quasi-ordered partial order, every upward-closed set is the union of the principal filters of its finitely many minimal elements.
Higman's lemma [Hig52]: over a finite type the sublist order is a well-quasi-order.