Reference : [Becker-Weispfenning1993]

Formalization of Proposition 4.42

This section formalizes Proposition 4.42, which states the equivalence of three conditions for a preorder ≤ on a set M:

1. (i) ≤ has the Dickson property (every subset has a finite basis).
2. (ii) ≤ is a Well Quasi‑Order (every infinite sequence aₙ has i < j with aᵢ ≤ aⱼ).
3. (iii) For every nonempty N : Set M, the set of min‑classes minClasses N is finite and nonempty.

We define a predicate for (i) and show its equivalence to (ii), which is represented by the typeclass WellQuasiOrderedLE M. The equivalence is proven by relating both to condition (iii) using Mathlib’s wellQuasiOrderedLE_iff.

def HasDicksonProperty (M : Type u_1) [Preorder M] : Prop

Definition 4.39 The relation ≤ on M has the Dickson property (finite basis property). Every subset N of M has a finite subset B ⊆ N such that every element of N is greater than or equal to some element of B.

Equations

• HasDicksonProperty M = ∀ (N : Set M), ∃ (B : Set M), B.Finite ∧ B ⊆ N ∧ ∀ a ∈ N, ∃ b ∈ B, b ≤ a

def MinimalElements {M : Type u_1} [Preorder M] (N : Set M) : Set M

Minimal elements (MinimalElements)

Let N ⊆ M. An element a ∈ N is minimal in N if there is no b ∈ N with b < a, where < is the strict part of the preorder.

Equations

• MinimalElements N = {a : M | a ∈ N ∧ ∀ b ∈ N, ¬b < a}

def minClasses {M : Type u_1} [Preorder M] (N : Set M) : Set (Set M)

Min–classes (minClasses)

Fix N ⊆ M. We use the equivalence relation ≈ induced by antisymmetry: a ≈ b means a ≤ b ∧ b ≤ a.

A min–class of N is obtained by taking a minimal element a ∈ MinimalElements N and intersecting N with its ≈-equivalence class.

Equations

• minClasses N = {C : Set M | ∃ a ∈ MinimalElements N, C = {x : M | x ∈ N ∧ x ≈ a}}

theorem minClasses_restrict_le_subset {M : Type u_1} [Preorder M] {N : Set M} {a : M} : ∀ {x : a ∈ N}, minClasses {d : M | d ∈ N ∧ d ≤ a} ⊆ minClasses N

Lemma minClasses_restrict_le_subset

Let N ⊆ M and let a ∈ N. Consider the restricted subset

Nₐ := { d ∈ N | d ≤ a }.

Then every min–class of Nₐ is also a min–class of N, i.e.

minClasses Nₐ ⊆ minClasses N.

theorem finite_minClasses_implies_hasDicksonProperty {M : Type u_1} [Preorder M] (h : ∀ (N : Set M), N.Nonempty → (minClasses N).Finite ∧ (minClasses N).Nonempty) : HasDicksonProperty M

Lemma (iii) ⇒ (i): finiteness and nonemptiness of min‑classes implies Dickson Property. Shows that if for every nonempty (N : Set M) the set minClasses N is finite and nonempty (Condition iii), then every subset N has a finite basis (Condition i).

theorem HasDicksonProperty.to_wellQuasiOrderedLE {M : Type u_1} [Preorder M] (h : HasDicksonProperty M) : WellQuasiOrderedLE M

Lemma (i) ⇒ (ii): A poset with the Dickson property is well‐quasi‐ordered.

theorem WellQuasiOrderedLE.minClasses_finite_and_nonempty {M : Type u_1} [Preorder M] (h_wqo : WellQuasiOrderedLE M) (N : Set M) : N.Nonempty → (minClasses N).Finite ∧ (minClasses N).Nonempty

(ii) ⇒ (iii): A Well Quasi-Ordered preorder has only finitely many, but at least one, min‑classes in any nonempty subset.

theorem HasDicksonProperty_iff_WellQuasiOrderedLE {M : Type u_1} [Preorder M] : HasDicksonProperty M ↔ WellQuasiOrderedLE M

Theorem (Proposition 4.42, conditions (i) and (ii)).

For a preorder ≤ on M, the following are equivalent:

• (i) ≤ has the Dickson property (finite basis property): for every subset N ⊆ M there exists a finite subset B ⊆ N such that for every a ∈ N there exists b ∈ B with b ≤ a.

• (ii) ≤ is a well quasi-order (wqo): for every sequence a : ℕ → M there exist indices i < j with a i ≤ a j.

This theorem formalises the equivalence (i) ↔ (ii) from Proposition 4.42.