From 39e796fa42b96e76cfd8bb68ac2c0526fed59446 Mon Sep 17 00:00:00 2001 From: "Hagb (Junyu Guo)" Date: Mon, 25 May 2026 04:30:52 +0800 Subject: [PATCH 1/5] feat(Order/WellQuasiOrder): `WellQuasiOrdered` if onto homomorphous from a `WellQuasiOrdered` relation --- Mathlib/Order/WellQuasiOrder.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean index 356495c8788a40..a1da7efff7cdd0 100644 --- a/Mathlib/Order/WellQuasiOrder.lean +++ b/Mathlib/Order/WellQuasiOrder.lean @@ -113,6 +113,13 @@ theorem RelIso.wellQuasiOrdered_iff {α β} {r : α → α → Prop} {s : β → congr! with g a b simp [f.map_rel_iff] +theorem RelHom.wellQuasiOrdered_of_wellQuasiOrdered_of_surjective {α β} {r : α → α → Prop} + {s : β → β → Prop} (h : WellQuasiOrdered r) (f : r →r s) (hf : Function.Surjective f) : + WellQuasiOrdered s := by + intro seq + have ⟨_, _, hmn⟩ := h (Function.surjInv hf ∘ seq) + exact ⟨_, _, hmn.1, by simpa [Function.surjInv_eq] using f.map_rel hmn.2⟩ + /-- A typeclass for an order with a well-quasi-ordered `≤` relation. Note that this is unlike `WellFoundedLT`, which instead takes a `<` relation. -/ @@ -178,6 +185,15 @@ theorem wellQuasiOrderedLE_iff : instance [WellQuasiOrderedLE α] [Preorder β] [WellQuasiOrderedLE β] : WellQuasiOrderedLE (α × β) := ⟨wellQuasiOrdered_le.prod wellQuasiOrdered_le⟩ +theorem Monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β] + [WellQuasiOrderedLE α] {f : α → β} (mono : Monotone f) (hf : Function.Surjective f) : + WellQuasiOrderedLE β := + ⟨RelHom.wellQuasiOrdered_of_wellQuasiOrdered_of_surjective wellQuasiOrdered_le ⟨_, (mono ·)⟩ hf⟩ + +theorem OrderHom.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β] + [WellQuasiOrderedLE α] (f : α →o β) (hf : Function.Surjective f) : + WellQuasiOrderedLE β := f.monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective hf + end Preorder section LinearOrder From f79b7f7ad2cca9cf148fd1556fe0a1a97aa8c6a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hagb=20=28Junyu=20Guo=20=E9=83=AD=E4=BF=8A=E4=BD=99=29?= Date: Tue, 7 Jul 2026 10:19:58 +0200 Subject: [PATCH 2/5] Update Mathlib/Order/WellQuasiOrder.lean Co-authored-by: Aaron Liu --- Mathlib/Order/WellQuasiOrder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean index a1da7efff7cdd0..71ccf31f9d7e3b 100644 --- a/Mathlib/Order/WellQuasiOrder.lean +++ b/Mathlib/Order/WellQuasiOrder.lean @@ -113,7 +113,7 @@ theorem RelIso.wellQuasiOrdered_iff {α β} {r : α → α → Prop} {s : β → congr! with g a b simp [f.map_rel_iff] -theorem RelHom.wellQuasiOrdered_of_wellQuasiOrdered_of_surjective {α β} {r : α → α → Prop} +theorem WellQuasiOrdered.of_surjective {α β} {r : α → α → Prop} {s : β → β → Prop} (h : WellQuasiOrdered r) (f : r →r s) (hf : Function.Surjective f) : WellQuasiOrdered s := by intro seq From e5a03fb496f8c1a5cdfcf4253ab2a19c398a698f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hagb=20=28Junyu=20Guo=20=E9=83=AD=E4=BF=8A=E4=BD=99=29?= Date: Tue, 7 Jul 2026 10:20:13 +0200 Subject: [PATCH 3/5] Update Mathlib/Order/WellQuasiOrder.lean Co-authored-by: Anne Baanen --- Mathlib/Order/WellQuasiOrder.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean index 71ccf31f9d7e3b..66a9d6f4ffd7e9 100644 --- a/Mathlib/Order/WellQuasiOrder.lean +++ b/Mathlib/Order/WellQuasiOrder.lean @@ -117,8 +117,8 @@ theorem WellQuasiOrdered.of_surjective {α β} {r : α → α → Prop} {s : β → β → Prop} (h : WellQuasiOrdered r) (f : r →r s) (hf : Function.Surjective f) : WellQuasiOrdered s := by intro seq - have ⟨_, _, hmn⟩ := h (Function.surjInv hf ∘ seq) - exact ⟨_, _, hmn.1, by simpa [Function.surjInv_eq] using f.map_rel hmn.2⟩ + have ⟨_, _, hle, hr⟩ := h (Function.surjInv hf ∘ seq) + exact ⟨_, _, hle, by simpa [Function.surjInv_eq] using f.map_rel hr⟩ /-- A typeclass for an order with a well-quasi-ordered `≤` relation. From ff497d2ba4cfda6a06cc944ecdb2d7fc3fb99b8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hagb=20=28Junyu=20Guo=20=E9=83=AD=E4=BF=8A=E4=BD=99=29?= Date: Tue, 7 Jul 2026 10:43:23 +0200 Subject: [PATCH 4/5] update name --- Mathlib/Order/WellQuasiOrder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean index 005e5bb8bc375e..00710d858cc2ce 100644 --- a/Mathlib/Order/WellQuasiOrder.lean +++ b/Mathlib/Order/WellQuasiOrder.lean @@ -188,7 +188,7 @@ instance [WellQuasiOrderedLE α] [Preorder β] [WellQuasiOrderedLE β] : WellQua theorem Monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β] [WellQuasiOrderedLE α] {f : α → β} (mono : Monotone f) (hf : Function.Surjective f) : WellQuasiOrderedLE β := - ⟨RelHom.wellQuasiOrdered_of_wellQuasiOrdered_of_surjective wellQuasiOrdered_le ⟨_, (mono ·)⟩ hf⟩ + ⟨wellQuasiOrdered_le.of_surjective ⟨_, (mono ·)⟩ hf⟩ theorem OrderHom.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β] [WellQuasiOrderedLE α] (f : α →o β) (hf : Function.Surjective f) : From 304fb6161c850bc7929d02cc10809408a05fcb11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hagb=20=28Junyu=20Guo=20=E9=83=AD=E4=BF=8A=E4=BD=99=29?= Date: Tue, 7 Jul 2026 12:10:53 +0200 Subject: [PATCH 5/5] Update Mathlib/Order/WellQuasiOrder.lean Co-authored-by: Anne Baanen --- Mathlib/Order/WellQuasiOrder.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean index 00710d858cc2ce..0d34ea4abd0651 100644 --- a/Mathlib/Order/WellQuasiOrder.lean +++ b/Mathlib/Order/WellQuasiOrder.lean @@ -192,7 +192,8 @@ theorem Monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorde theorem OrderHom.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β] [WellQuasiOrderedLE α] (f : α →o β) (hf : Function.Surjective f) : - WellQuasiOrderedLE β := f.monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective hf + WellQuasiOrderedLE β := + f.monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective hf end Preorder