Well-quasi-order
IsWellQuasiOrderdef
A relation is a well-quasi-order when every infinite sequence contains a pair, in order, that the relation relates. Kruskal's tree theorem and the graph-minor theorem are both statements that a particular relation is one.
def IsWellQuasiOrder {α : Type*} (r : α → α → Prop) : Prop :=
∀ f : ℕ → α, ∃ i j : ℕ, i < j ∧ r (f i) (f j)From Mathlib
import Conjectura.Defs.Mathematics.Logic.WellQuasiOrder · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors