Well-quasi-order

Conjectura.Defs.Mathematics.Logic.WellQuasiOrder

/-
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
-/
import Mathlib.Order.Defs.PartialOrder
import Mathlib.Data.Nat.Notation

/-! # Well-quasi-order -/

namespace Conjectura.Logic

/-- 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)

end Conjectura.Logic