From 77fa41e6fababcd5fd66d8ccbdfe10a82cead6fb Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 24 May 2026 14:35:52 -0600 Subject: [PATCH 1/6] add --- .../SetTheory/Cardinal/Cofinality/Basic.lean | 4 ++++ .../Cardinal/Cofinality/Ordinal.lean | 21 ++++++++++++------- Mathlib/SetTheory/Ordinal/Basic.lean | 4 ++++ 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean index ff288badfea0f4..b4c26e23b986a1 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean @@ -48,6 +48,7 @@ theorem le_cof_iff {c : Cardinal} : c ≤ cof α ↔ ∀ s : Set α, IsCofinal s @[deprecated (since := "2026-02-18")] alias le_cof := le_cof_iff variable (α) in +/-- Every well-order has a cofinal subset of cardinal `cof α`. -/ theorem cof_eq : ∃ s : Set α, IsCofinal s ∧ #s = cof α := by obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s exact ⟨s.1, s.2, hs⟩ @@ -131,6 +132,9 @@ theorem cof_congr_of_strictMono {f : α → γ} (hf : StrictMono f) (hf' : IsCof cof α = cof γ := by simpa using lift_cof_congr_of_strictMono hf hf' +theorem cof_eq_of_isCofinal {s : Set α} (hs : IsCofinal s) : cof s = cof α := + cof_congr_of_strictMono (Subtype.strictMono_coe _) (by simpa) + @[simp] theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩ diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 7fbb74e6cd1928..eb19124ca85c03 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -151,7 +151,9 @@ theorem cof_omega0 : cof ω = ℵ₀ := @[deprecated (since := "2026-02-18")] alias cof_eq_one_iff_is_succ := cof_eq_one_iff -theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : +variable (α) in +/-- Every well-order has a cofinal subset of order type `(cof α).ord`. -/ +theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by obtain ⟨s, hs, hs'⟩ := Order.cof_eq α obtain ⟨r, hr, hr'⟩ := exists_ord_eq s @@ -166,16 +168,21 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : · obtain ⟨x, z, hz, rfl⟩ := x exact (hz _ hxy').asymm hxy +/-- Every cofinal set has a cofinal subset of order type `(cof α).ord`. -/ +theorem ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : + ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by + obtain ⟨t, ht, ht'⟩ := ord_cof_eq s + rw [cof_eq_of_isCofinal hs] at ht' + refine ⟨t, ?_, hs.trans ht, ?_⟩ + · simp + · rw [← ht'] + exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinal_type_eq.symm + @[simp] theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] : (Order.cof α).ord.cof = Order.cof α := by obtain ⟨s, hs, hs'⟩ := ord_cof_eq α - rw [← hs', cof_type] - apply le_antisymm - · rw [← card_ord (Order.cof α), ← hs', card_type] - exact cof_le_cardinalMk s - · rw [le_cof_iff] - exact fun t ht ↦ (cof_le (hs.trans ht)).trans_eq (mk_image_eq Subtype.val_injective) + rw [← hs', cof_type, cof_eq_of_isCofinal hs] @[simp] theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 3ae32b127dfa6e..ab2496f5c9cb1e 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -169,6 +169,10 @@ theorem _root_.RelIso.ordinal_type_eq {α β} {r : α → α → Prop} {s : β [IsWellOrder β s] (h : r ≃r s) : type r = type s := type_eq.2 ⟨h⟩ +theorem _root_.OrderIso.ordinal_type_eq {α β} [LinearOrder α] [LinearOrder β] + [WellFoundedLT α] [WellFoundedLT β] (h : α ≃o β) : typeLT α = typeLT β := + h.toRelIsoLT.ordinal_type_eq + theorem type_eq_zero_of_empty (r) [IsWellOrder α r] [IsEmpty α] : type r = 0 := (RelIso.relIsoOfIsEmpty r _).ordinal_type_eq From a455b82d7ed3bce9824a24c860f40e53923ea06a Mon Sep 17 00:00:00 2001 From: vihdzp Date: Mon, 25 May 2026 09:44:35 -0600 Subject: [PATCH 2/6] rename --- Mathlib/SetTheory/Cardinal/Aleph.lean | 2 +- .../Cardinal/Cofinality/Ordinal.lean | 2 +- Mathlib/SetTheory/Ordinal/Basic.lean | 29 ++++++++++--------- 3 files changed, 18 insertions(+), 15 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean index 5d077051de1e5a..e70db812cdbc6a 100644 --- a/Mathlib/SetTheory/Cardinal/Aleph.lean +++ b/Mathlib/SetTheory/Cardinal/Aleph.lean @@ -302,7 +302,7 @@ theorem ord_preAleph (o : Ordinal) : (preAleph o).ord = preOmega o := by @[simp] theorem _root_.Ordinal.type_lt_cardinal : typeLT Cardinal = Ordinal.univ.{u, u + 1} := by - simpa using preAleph.symm.toRelIsoLT.ordinal_type_eq + simpa using preAleph.symm.ordinalType_congr @[deprecated (since := "2026-03-20")] alias type_cardinal := type_lt_cardinal diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index eb19124ca85c03..78755c279e8b3a 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -176,7 +176,7 @@ theorem ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} refine ⟨t, ?_, hs.trans ht, ?_⟩ · simp · rw [← ht'] - exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinal_type_eq.symm + exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.symm @[simp] theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] : diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index ab2496f5c9cb1e..d7ff5d1f9b2d73 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -165,16 +165,19 @@ theorem type_eq {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWel type r = type s ↔ Nonempty (r ≃r s) := Quotient.eq' -theorem _root_.RelIso.ordinal_type_eq {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] +theorem _root_.RelIso.ordinalType_congr {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) : type r = type s := type_eq.2 ⟨h⟩ -theorem _root_.OrderIso.ordinal_type_eq {α β} [LinearOrder α] [LinearOrder β] +@[deprecated (since := "2026-05-25")] +alias _root_.RelIso.ordinal_type_eq := RelIso.ordinalType_congr + +theorem _root_.OrderIso.ordinalType_congr {α β} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] [WellFoundedLT β] (h : α ≃o β) : typeLT α = typeLT β := - h.toRelIsoLT.ordinal_type_eq + h.toRelIsoLT.ordinalType_congr theorem type_eq_zero_of_empty (r) [IsWellOrder α r] [IsEmpty α] : type r = 0 := - (RelIso.relIsoOfIsEmpty r _).ordinal_type_eq + (RelIso.relIsoOfIsEmpty r _).ordinalType_congr @[simp] theorem type_eq_zero_iff_isEmpty [IsWellOrder α r] : type r = 0 ↔ IsEmpty α := by @@ -195,7 +198,7 @@ theorem type_empty : type (@emptyRelation Empty) = 0 := theorem type_eq_one_of_unique (r) [IsWellOrder α r] [Nonempty α] [Subsingleton α] : type r = 1 := by cases nonempty_unique α - exact (RelIso.ofUniqueOfIrrefl r _).ordinal_type_eq + exact (RelIso.ofUniqueOfIrrefl r _).ordinalType_congr @[simp] theorem type_eq_one_iff_unique [IsWellOrder α r] : type r = 1 ↔ Nonempty (Unique α) := @@ -403,7 +406,7 @@ def typein (r : α → α → Prop) [IsWellOrder α r] : @PrincipalSeg α Ordina exact (PrincipalSeg.ofElement _ _).ordinal_type_lt · refine inductionOn a ?_ rintro β s wo ⟨g⟩ - exact ⟨_, g.subrelIso.ordinal_type_eq⟩ + exact ⟨_, g.subrelIso.ordinalType_congr⟩ @[simp] theorem type_subrel (r : α → α → Prop) [IsWellOrder α r] (a : α) : @@ -424,7 +427,7 @@ theorem typein_lt_self {o : Ordinal} (i : o.ToType) : typein (α := o.ToType) ( @[simp] theorem typein_top {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≺i s) : typein s f.top = type r := - f.subrelIso.ordinal_type_eq + f.subrelIso.ordinalType_congr @[simp] theorem typein_lt_typein (r : α → α → Prop) [IsWellOrder α r] {a b : α} : @@ -652,12 +655,12 @@ theorem type_lt_ulift [LinearOrder α] [WellFoundedLT α] : theorem _root_.RelIso.ordinal_lift_type_eq {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) : lift.{v} (type r) = lift.{u} (type s) := ((RelIso.preimage Equiv.ulift r).trans <| - f.trans (RelIso.preimage Equiv.ulift s).symm).ordinal_type_eq + f.trans (RelIso.preimage Equiv.ulift s).symm).ordinalType_congr @[simp] theorem type_preimage {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : type (f ⁻¹'o r) = type r := - (RelIso.preimage f r).ordinal_type_eq + (RelIso.preimage f r).ordinalType_congr @[simp] theorem type_lift_preimage (r : α → α → Prop) [IsWellOrder α r] @@ -823,11 +826,11 @@ the addition, together with properties of the other operations, are proved in every element of `o₁` is smaller than every element of `o₂`. -/ instance add : Add Ordinal.{u} := ⟨fun o₁ o₂ => Quotient.liftOn₂ o₁ o₂ (fun ⟨_, r, _⟩ ⟨_, s, _⟩ => type (Sum.Lex r s)) - fun _ _ _ _ ⟨f⟩ ⟨g⟩ => (RelIso.sumLexCongr f g).ordinal_type_eq⟩ + fun _ _ _ _ ⟨f⟩ ⟨g⟩ => (RelIso.sumLexCongr f g).ordinalType_congr⟩ instance addMonoidWithOne : AddMonoidWithOne Ordinal.{u} where - zero_add o := inductionOn o fun α _ _ => (RelIso.emptySumLex _ _).ordinal_type_eq - add_zero o := inductionOn o fun α _ _ => (RelIso.sumLexEmpty _ _).ordinal_type_eq + zero_add o := inductionOn o fun α _ _ => (RelIso.emptySumLex _ _).ordinalType_congr + add_zero o := inductionOn o fun α _ _ => (RelIso.sumLexEmpty _ _).ordinalType_congr add_assoc o₁ o₂ o₃ := Quotient.inductionOn₃ o₁ o₂ o₃ fun _ _ _ ↦ Quot.sound ⟨⟨sumAssoc .., by simp⟩⟩ nsmul := nsmulRec @@ -869,7 +872,7 @@ instance existsAddOfLE : ExistsAddOfLE Ordinal where exists_add_of_le {a b} := by refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_ obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso - exact ⟨type t, g.ordinal_type_eq.symm⟩ + exact ⟨type t, g.ordinalType_congr.symm⟩ instance canonicallyOrderedAdd : CanonicallyOrderedAdd Ordinal where le_add_self a b := by simpa using add_le_add_left bot_le a From db455dbe60f753aacc482b6d9a251460357526d8 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Mon, 25 May 2026 09:44:50 -0600 Subject: [PATCH 3/6] longline --- Mathlib/SetTheory/Ordinal/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index d7ff5d1f9b2d73..ea07a6d7987f0a 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -165,8 +165,8 @@ theorem type_eq {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWel type r = type s ↔ Nonempty (r ≃r s) := Quotient.eq' -theorem _root_.RelIso.ordinalType_congr {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] - [IsWellOrder β s] (h : r ≃r s) : type r = type s := +theorem _root_.RelIso.ordinalType_congr {α β} {r : α → α → Prop} {s : β → β → Prop} + [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) : type r = type s := type_eq.2 ⟨h⟩ @[deprecated (since := "2026-05-25")] From e7d58c7a74bfc4e566c82693a81e71171feff6c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= Date: Mon, 25 May 2026 12:33:16 -0600 Subject: [PATCH 4/6] Update Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 78755c279e8b3a..e9009b91f7ac12 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -169,7 +169,7 @@ theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : exact (hz _ hxy').asymm hxy /-- Every cofinal set has a cofinal subset of order type `(cof α).ord`. -/ -theorem ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : +theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by obtain ⟨t, ht, ht'⟩ := ord_cof_eq s rw [cof_eq_of_isCofinal hs] at ht' From 0ebcdb1a811aa48281203217809b4a4a5daf1633 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Mon, 25 May 2026 15:28:03 -0600 Subject: [PATCH 5/6] fix --- Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index e9009b91f7ac12..c61ac4823085da 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -169,8 +169,8 @@ theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : exact (hz _ hxy').asymm hxy /-- Every cofinal set has a cofinal subset of order type `(cof α).ord`. -/ -theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : - ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by +theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] + {s : Set α} (hs : IsCofinal s) : ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by obtain ⟨t, ht, ht'⟩ := ord_cof_eq s rw [cof_eq_of_isCofinal hs] at ht' refine ⟨t, ?_, hs.trans ht, ?_⟩ From 3c5712058782e7e9f2251d618310f412ce0a564c Mon Sep 17 00:00:00 2001 From: vihdzp Date: Mon, 25 May 2026 23:29:44 -0600 Subject: [PATCH 6/6] fix --- Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index c61ac4823085da..e96e8b5fa20c78 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -153,7 +153,7 @@ theorem cof_omega0 : cof ω = ℵ₀ := variable (α) in /-- Every well-order has a cofinal subset of order type `(cof α).ord`. -/ -theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : +theorem exists_ord_cof_eq [LinearOrder α] [WellFoundedLT α] : ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by obtain ⟨s, hs, hs'⟩ := Order.cof_eq α obtain ⟨r, hr, hr'⟩ := exists_ord_eq s @@ -168,10 +168,12 @@ theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : · obtain ⟨x, z, hz, rfl⟩ := x exact (hz _ hxy').asymm hxy +@[deprecated (since := "2026-05-25")] alias ord_cof_eq := exists_ord_cof_eq + /-- Every cofinal set has a cofinal subset of order type `(cof α).ord`. -/ theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by - obtain ⟨t, ht, ht'⟩ := ord_cof_eq s + obtain ⟨t, ht, ht'⟩ := exists_ord_cof_eq s rw [cof_eq_of_isCofinal hs] at ht' refine ⟨t, ?_, hs.trans ht, ?_⟩ · simp @@ -181,7 +183,7 @@ theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] @[simp] theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] : (Order.cof α).ord.cof = Order.cof α := by - obtain ⟨s, hs, hs'⟩ := ord_cof_eq α + obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α rw [← hs', cof_type, cof_eq_of_isCofinal hs] @[simp] @@ -649,7 +651,7 @@ theorem lt_power_cof_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : c < c ^ c.ord.cof have : NoMaxOrder α := by rw [← isSuccPrelimit_type_lt_iff, ← hα] exact (isSuccLimit_ord hc).isSuccPrelimit - obtain ⟨s, hs, hs'⟩ := ord_cof_eq α + obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const'] refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα) rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]