From 117691eb5b98dc08454dcaf74374449b90ed2aed Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Fri, 16 Jan 2026 20:19:56 +1100 Subject: [PATCH 01/13] Adding `Order.Types.Defs` and moving `LinOrd` definition --- Mathlib/Order/Defs/LinearOrder.lean | 21 +++ Mathlib/Order/Types/Defs.lean | 235 ++++++++++++++++++++++++++++ 2 files changed, 256 insertions(+) create mode 100644 Mathlib/Order/Types/Defs.lean diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean index 78728ccb080cb6..b807994e66f1eb 100644 --- a/Mathlib/Order/Defs/LinearOrder.lean +++ b/Mathlib/Order/Defs/LinearOrder.lean @@ -236,4 +236,25 @@ instance : Std.LawfulBCmp (compare (α := α)) where end Ord +/-- The category of linear orders. -/ +structure LinOrd where + /-- Construct a bundled `LinOrd` from the underlying type and typeclass. -/ + of :: + /-- The underlying linearly ordered type. -/ + (carrier : Type*) + [str : LinearOrder carrier] + +attribute [instance] LinOrd.str + +initialize_simps_projections LinOrd (carrier → coe, -str) + +namespace LinOrd + +instance : CoeSort LinOrd (Type _) := + ⟨LinOrd.carrier⟩ + +attribute [coe] LinOrd.carrier + +end LinOrd + end LinearOrder diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean new file mode 100644 index 00000000000000..9673cd2615ee59 --- /dev/null +++ b/Mathlib/Order/Types/Defs.lean @@ -0,0 +1,235 @@ +/- +Copyright (c) 2025 Yan Yablonovskiy. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yan Yablonovskiy +-/ +module + +public import Mathlib.Order.Hom.Basic + +/-! +# Order types + +Order types are defined as the quotient of linear orders under order isomorphism. They are endowed +with a preorder, where an OrderType is smaller than another one there is an order embedding +into it. + +## Main definitions + +* `OrderType`: the type of OrderTypes (in a given universe) +* `OrderType.type α`: given a type `α` with a linear order, this is the corresponding OrderType, + +A preorder with a bottom element is registered on order types, where `⊥` is +`0`, the order type corresponding to the empty type. + +## Notation + +The following are notations in the `OrderType` namespace: + +* `ω` is a notation for the order type of `ℕ` with its natural order. + +## References + +* +* Dauben, J. W. Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton, + NJ: Princeton University Press, 1990. +* Enderton, Herbert B. Elements of Set Theory. United Kingdom: Academic Press, 1977. + +## Tags + +order type, order isomorphism, linear order +-/ + +@[expose] public noncomputable section + +open Function Set Equiv Order + +universe u v w w' + +variable {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} + +/-- Equivalence relation on linear orders on arbitrary types in universe `u`, given by order +isomorphism. -/ +instance OrderType.instSetoid : Setoid LinOrd where + r := fun lin_ord₁ lin_ord₂ ↦ Nonempty (lin_ord₁ ≃o lin_ord₂) + iseqv := ⟨fun _ ↦ ⟨.refl _⟩, fun ⟨e⟩ ↦ ⟨e.symm⟩, fun ⟨e₁⟩ ⟨e₂⟩ ↦ ⟨e₁.trans e₂⟩⟩ + +/-- `OrderType.{u}` is the type of linear orders in `Type u`, up to order isomorphism. -/ +@[pp_with_univ] +def OrderType : Type (u + 1) := + Quotient OrderType.instSetoid + +namespace OrderType + +/-- A "canonical" type order-isomorphic to the order type `o`, living in the same universe. +This is defined through the axiom of choice. -/ +public def ToType (o : OrderType) : Type u := + o.out.carrier + +instance (o : OrderType) : LinearOrder o.ToType := + o.out.str + +/-! ### Basic properties of the order type -/ + +/-- The order type of the linear order on `α`. -/ +def type (α : Type u) [LinearOrder α] : OrderType := + ⟦⟨α⟩⟧ + +instance zero : Zero OrderType where + zero := type PEmpty + +instance inhabited : Inhabited OrderType := + ⟨0⟩ +instance : One OrderType where + one := type PUnit + +lemma one_def : (1 : OrderType) = type PUnit := rfl + +@[simp] +theorem type_toType (o : OrderType) : type o.ToType = o := surjInv_eq Quot.exists_rep o + +theorem type_eq {α β} [LinearOrder α] [LinearOrder β] : + type α = type β ↔ Nonempty (α ≃o β) := + Quotient.eq' + +theorem _root_.RelIso.orderType_eq {α β} [LinearOrder α] + [LinearOrder β] (h : α ≃o β) : type α = type β := + type_eq.2 ⟨h⟩ + +@[simp] +theorem type_of_isEmpty [LinearOrder α] [IsEmpty α] : type α = 0 := + (OrderIso.ofIsEmpty α PEmpty).orderType_eq + +@[simp] +theorem type_eq_zero [LinearOrder α] : type α = 0 ↔ IsEmpty α := + ⟨fun h ↦ + let ⟨s⟩ := type_eq.1 h + s.toEquiv.isEmpty, + @type_of_isEmpty α _⟩ + +theorem type_ne_zero_iff [LinearOrder α] : type α ≠ 0 ↔ Nonempty α := by simp + +theorem type_ne_zero [LinearOrder α] [h : Nonempty α] : type α ≠ 0 := + type_ne_zero_iff.2 h + +@[simp] +theorem type_of_unique [LinearOrder α] [Nonempty α] [Subsingleton α] : type α = 1 := by + cases nonempty_unique α + exact (OrderIso.ofUnique α _).orderType_eq + +@[simp] +theorem type_eq_one [LinearOrder α] : type α = 1 ↔ Nonempty (Unique α) := + ⟨fun h ↦ let ⟨s⟩ := type_eq.1 h; ⟨s.toEquiv.unique⟩, + fun ⟨_⟩ ↦ type_of_unique⟩ + +@[simp] +theorem isEmpty_toType_iff {o : OrderType} : IsEmpty o.ToType ↔ o = 0 := by + rw [← @type_eq_zero o.ToType, type_toType] + +instance isEmpty_toType_zero : IsEmpty (ToType 0) := + isEmpty_toType_iff.2 rfl + +@[simp] +theorem nonempty_toType_iff {o : OrderType} : Nonempty o.ToType ↔ o ≠ 0 := by + rw [← @type_ne_zero_iff o.ToType, type_toType] + +protected theorem one_ne_zero : (1 : OrderType) ≠ 0 := + type_ne_zero + +instance nontrivial : Nontrivial OrderType.{u} := + ⟨⟨1, 0, OrderType.one_ne_zero⟩⟩ + +/-- `Quotient.inductionOn` specialized to `OrderType`. -/ +@[elab_as_elim] +theorem inductionOn {C : OrderType → Prop} (o : OrderType) + (H : ∀ α [LinearOrder α], C (type α)) : C o := + Quot.inductionOn o (fun α ↦ H α) + +/-- `Quotient.inductionOn₂` specialized to `OrderType`. -/ +@[elab_as_elim] +theorem inductionOn₂ {C : OrderType → OrderType → Prop} (o₁ o₂ : OrderType) + (H : ∀ α [LinearOrder α] β [LinearOrder β], C (type α) (type β)) : C o₁ o₂ := + Quotient.inductionOn₂ o₁ o₂ fun α β ↦ H α β + +/-- `Quotient.inductionOn₃` specialized to `OrderType`. -/ +@[elab_as_elim] +theorem inductionOn₃ {C : OrderType → OrderType → OrderType → Prop} (o₁ o₂ o₃ : OrderType) + (H : ∀ α [LinearOrder α] β [LinearOrder β] γ [LinearOrder γ], + C (type α) (type β) (type γ)) : C o₁ o₂ o₃ := + Quotient.inductionOn₃ o₁ o₂ o₃ fun α β γ ↦ + H α β γ + +/-- To define a function on `OrderType`, it suffices to define it on all linear orders. +-/ +def liftOn {δ : Sort v} (o : OrderType) (f : ∀ (α) [LinearOrder α], δ) + (c : ∀ (α) [LinearOrder α] (β) [LinearOrder β], + type α = type β → f α = f β) : δ := + Quotient.liftOn o (fun w ↦ f w) + fun w₁ w₂ h ↦ c w₁ w₂ (Quotient.sound h) + +@[simp] +theorem liftOn_type {δ : Sort v} (f : ∀ (α) [LinearOrder α], δ) + (c : ∀ (α) [LinearOrder α] (β) [LinearOrder β], + type α = type β → f α = f β) {γ} [inst : LinearOrder γ] : + liftOn (type γ) f c = f γ := rfl + +/-! ### The order on `OrderType` -/ + +/-- +The order is defined so that `type α ≤ type β` iff there exists an order embedding `α ↪o β`. +-/ +instance : Preorder OrderType where + le o₁ o₂ := + Quotient.liftOn₂ o₁ o₂ (fun r s ↦ Nonempty (r ↪o s)) + fun _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ propext + ⟨fun ⟨h⟩ ↦ ⟨(f.symm.toOrderEmbedding.trans h).trans g.toOrderEmbedding⟩, fun ⟨h⟩ ↦ + ⟨(f.toOrderEmbedding.trans h).trans g.symm.toOrderEmbedding⟩⟩ + le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) + le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ + +instance instNeZeroOne : NeZero (1 : OrderType) := + ⟨OrderType.one_ne_zero⟩ + +theorem type_le_type_iff {α β} [LinearOrder α] + [LinearOrder β] : type α ≤ type β ↔ Nonempty (α ↪o β) := + Iff.rfl + +theorem type_le_type {α β} + [LinearOrder α] [LinearOrder β] (h : α ↪o β) : type α ≤ type β := + ⟨h⟩ + +alias _root_.OrderEmbedding.type_le_type := type_le_type + +@[simp] +protected theorem zero_le (o : OrderType) : 0 ≤ o := + inductionOn o (fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type) + +instance instOrdBot : OrderBot OrderType where + bot := 0 + bot_le := OrderType.zero_le + +@[simp] +theorem bot_eq_zero : (⊥ : OrderType) = 0 := + rfl + +@[simp] +protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := + not_lt_bot + +#check lt_of_le_of_lt +#check lt_iff_le_not_ge + +@[simp] +theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := + ⟨ne_bot_of_gt, fun ho ↦ by simpa [@type_of_isEmpty PEmpty] using + (⟨⟨Function.Embedding.ofIsEmpty, by simp⟩, fun ⟨f⟩ ↦ PEmpty.elim + (f (Classical.choice (OrderType.nonempty_toType_iff.mpr ho)))⟩ : type PEmpty < type o.ToType)⟩ + +/-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ +public def omega0 : OrderType := type ℕ + +@[inherit_doc] +scoped notation "ω" => OrderType.omega0 +recommended_spelling "omega0" for "ω" in [omega0, «termω»] + +end OrderType From e08c49b035ad2dbce8af7aa647cd5682f6b60d1f Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Fri, 16 Jan 2026 21:21:14 +1100 Subject: [PATCH 02/13] Remove `LinOrd` from old location --- Mathlib/Order/Category/LinOrd.lean | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/Mathlib/Order/Category/LinOrd.lean b/Mathlib/Order/Category/LinOrd.lean index 363529bc99fc07..f564fdd58f46f9 100644 --- a/Mathlib/Order/Category/LinOrd.lean +++ b/Mathlib/Order/Category/LinOrd.lean @@ -20,25 +20,8 @@ open CategoryTheory universe u -/-- The category of linear orders. -/ -structure LinOrd where - /-- Construct a bundled `LinOrd` from the underlying type and typeclass. -/ - of :: - /-- The underlying linearly ordered type. -/ - (carrier : Type*) - [str : LinearOrder carrier] - -attribute [instance] LinOrd.str - -initialize_simps_projections LinOrd (carrier → coe, -str) - namespace LinOrd -instance : CoeSort LinOrd (Type _) := - ⟨LinOrd.carrier⟩ - -attribute [coe] LinOrd.carrier - set_option backward.privateInPublic true in /-- The type of morphisms in `LinOrd R`. -/ @[ext] From 6960dd6ac0dbcc3138f27bb1b2b813a2ba0024d4 Mon Sep 17 00:00:00 2001 From: Yan Yablonovskiy Date: Fri, 16 Jan 2026 21:34:50 +1100 Subject: [PATCH 03/13] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Defs/LinearOrder.lean | 4 +++- Mathlib/Order/Types/Defs.lean | 15 ++++++++------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/Mathlib/Order/Defs/LinearOrder.lean b/Mathlib/Order/Defs/LinearOrder.lean index b807994e66f1eb..1760d19e3260d5 100644 --- a/Mathlib/Order/Defs/LinearOrder.lean +++ b/Mathlib/Order/Defs/LinearOrder.lean @@ -236,7 +236,9 @@ instance : Std.LawfulBCmp (compare (α := α)) where end Ord -/-- The category of linear orders. -/ +/-- The category of linear orders. + +This will get reused to define `OrderType`. -/ structure LinOrd where /-- Construct a bundled `LinOrd` from the underlying type and typeclass. -/ of :: diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 9673cd2615ee59..5b8f330f379c7b 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -11,12 +11,12 @@ public import Mathlib.Order.Hom.Basic # Order types Order types are defined as the quotient of linear orders under order isomorphism. They are endowed -with a preorder, where an OrderType is smaller than another one there is an order embedding +with a preorder, where an OrderType is ≤ to another when there is an order embedding into it. ## Main definitions -* `OrderType`: the type of OrderTypes (in a given universe) +* `OrderType`: the type of order types (in a given universe) * `OrderType.type α`: given a type `α` with a linear order, this is the corresponding OrderType, A preorder with a bottom element is registered on order types, where `⊥` is @@ -40,7 +40,7 @@ The following are notations in the `OrderType` namespace: order type, order isomorphism, linear order -/ -@[expose] public noncomputable section +public noncomputable section open Function Set Equiv Order @@ -63,7 +63,7 @@ namespace OrderType /-- A "canonical" type order-isomorphic to the order type `o`, living in the same universe. This is defined through the axiom of choice. -/ -public def ToType (o : OrderType) : Type u := +def ToType (o : OrderType) : Type u := o.out.carrier instance (o : OrderType) : LinearOrder o.ToType := @@ -192,7 +192,7 @@ instance instNeZeroOne : NeZero (1 : OrderType) := theorem type_le_type_iff {α β} [LinearOrder α] [LinearOrder β] : type α ≤ type β ↔ Nonempty (α ↪o β) := - Iff.rfl + .rfl theorem type_le_type {α β} [LinearOrder α] [LinearOrder β] (h : α ↪o β) : type α ≤ type β := @@ -221,12 +221,13 @@ protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := @[simp] theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := - ⟨ne_bot_of_gt, fun ho ↦ by simpa [@type_of_isEmpty PEmpty] using + ⟨ne_bot_of_gt, fun ho ↦ by simpa using (⟨⟨Function.Embedding.ofIsEmpty, by simp⟩, fun ⟨f⟩ ↦ PEmpty.elim (f (Classical.choice (OrderType.nonempty_toType_iff.mpr ho)))⟩ : type PEmpty < type o.ToType)⟩ /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ -public def omega0 : OrderType := type ℕ +-- TODO: define `OrderType.lift` and redefine this using it. +public def omega0 : OrderType := type <| ULift ℕ @[inherit_doc] scoped notation "ω" => OrderType.omega0 From c1c3030191a8abb28c69084f63f8867074d4be02 Mon Sep 17 00:00:00 2001 From: Yan Yablonovskiy Date: Fri, 16 Jan 2026 21:37:06 +1100 Subject: [PATCH 04/13] Update Mathlib/Order/Types/Defs.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Types/Defs.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 5b8f330f379c7b..8e9f76983031e8 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -216,9 +216,6 @@ theorem bot_eq_zero : (⊥ : OrderType) = 0 := protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := not_lt_bot -#check lt_of_le_of_lt -#check lt_iff_le_not_ge - @[simp] theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := ⟨ne_bot_of_gt, fun ho ↦ by simpa using From 128541e9aa94b82c452b8ef8019325db0a1e055f Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Fri, 16 Jan 2026 22:39:34 +1100 Subject: [PATCH 05/13] Review suggestions --- Mathlib/Order/Types/Defs.lean | 40 +++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 8e9f76983031e8..5a2605e1108677 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -55,7 +55,7 @@ instance OrderType.instSetoid : Setoid LinOrd where iseqv := ⟨fun _ ↦ ⟨.refl _⟩, fun ⟨e⟩ ↦ ⟨e.symm⟩, fun ⟨e₁⟩ ⟨e₂⟩ ↦ ⟨e₁.trans e₂⟩⟩ /-- `OrderType.{u}` is the type of linear orders in `Type u`, up to order isomorphism. -/ -@[pp_with_univ] +@[pp_with_univ, no_expose] def OrderType : Type (u + 1) := Quotient OrderType.instSetoid @@ -63,28 +63,32 @@ namespace OrderType /-- A "canonical" type order-isomorphic to the order type `o`, living in the same universe. This is defined through the axiom of choice. -/ +@[no_expose] def ToType (o : OrderType) : Type u := o.out.carrier -instance (o : OrderType) : LinearOrder o.ToType := +@[no_expose] +local instance (o : OrderType) : LinearOrder o.ToType := o.out.str /-! ### Basic properties of the order type -/ /-- The order type of the linear order on `α`. -/ +@[no_expose] def type (α : Type u) [LinearOrder α] : OrderType := ⟦⟨α⟩⟧ -instance zero : Zero OrderType where +@[no_expose] +instance : Zero OrderType where zero := type PEmpty instance inhabited : Inhabited OrderType := ⟨0⟩ + +@[no_expose] instance : One OrderType where one := type PUnit -lemma one_def : (1 : OrderType) = type PUnit := rfl - @[simp] theorem type_toType (o : OrderType) : type o.ToType = o := surjInv_eq Quot.exists_rep o @@ -123,14 +127,11 @@ theorem type_eq_one [LinearOrder α] : type α = 1 ↔ Nonempty (Unique α) := fun ⟨_⟩ ↦ type_of_unique⟩ @[simp] -theorem isEmpty_toType_iff {o : OrderType} : IsEmpty o.ToType ↔ o = 0 := by +private theorem isEmpty_toType_iff {o : OrderType} : IsEmpty o.ToType ↔ o = 0 := by rw [← @type_eq_zero o.ToType, type_toType] -instance isEmpty_toType_zero : IsEmpty (ToType 0) := - isEmpty_toType_iff.2 rfl - @[simp] -theorem nonempty_toType_iff {o : OrderType} : Nonempty o.ToType ↔ o ≠ 0 := by +private theorem nonempty_toType_iff {o : OrderType} : Nonempty o.ToType ↔ o ≠ 0 := by rw [← @type_ne_zero_iff o.ToType, type_toType] protected theorem one_ne_zero : (1 : OrderType) ≠ 0 := @@ -171,20 +172,21 @@ def liftOn {δ : Sort v} (o : OrderType) (f : ∀ (α) [LinearOrder α], δ) theorem liftOn_type {δ : Sort v} (f : ∀ (α) [LinearOrder α], δ) (c : ∀ (α) [LinearOrder α] (β) [LinearOrder β], type α = type β → f α = f β) {γ} [inst : LinearOrder γ] : - liftOn (type γ) f c = f γ := rfl + liftOn (type γ) f c = f γ := by rfl /-! ### The order on `OrderType` -/ /-- The order is defined so that `type α ≤ type β` iff there exists an order embedding `α ↪o β`. -/ +@[no_expose] instance : Preorder OrderType where le o₁ o₂ := Quotient.liftOn₂ o₁ o₂ (fun r s ↦ Nonempty (r ↪o s)) fun _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ propext ⟨fun ⟨h⟩ ↦ ⟨(f.symm.toOrderEmbedding.trans h).trans g.toOrderEmbedding⟩, fun ⟨h⟩ ↦ ⟨(f.toOrderEmbedding.trans h).trans g.symm.toOrderEmbedding⟩⟩ - le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) + le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ instance instNeZeroOne : NeZero (1 : OrderType) := @@ -198,6 +200,10 @@ theorem type_le_type {α β} [LinearOrder α] [LinearOrder β] (h : α ↪o β) : type α ≤ type β := ⟨h⟩ +theorem type_lt_type {α β} + [LinearOrder α] [LinearOrder β] (h : α ↪o β) (hne : ¬(Nonempty (β ↪o α))) : type α < type β := + ⟨⟨h⟩,hne⟩ + alias _root_.OrderEmbedding.type_le_type := type_le_type @[simp] @@ -218,13 +224,15 @@ protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := @[simp] theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := - ⟨ne_bot_of_gt, fun ho ↦ by simpa using - (⟨⟨Function.Embedding.ofIsEmpty, by simp⟩, fun ⟨f⟩ ↦ PEmpty.elim - (f (Classical.choice (OrderType.nonempty_toType_iff.mpr ho)))⟩ : type PEmpty < type o.ToType)⟩ + ⟨ne_bot_of_gt, fun ho ↦ by + convert type_lt_type (α := PEmpty) (β := o.ToType) ⟨Function.Embedding.ofIsEmpty, by simp⟩ + (fun ⟨f⟩ ↦ PEmpty.elim (f (Classical.choice (OrderType.nonempty_toType_iff.mpr ho)))) + simp⟩ /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ -- TODO: define `OrderType.lift` and redefine this using it. -public def omega0 : OrderType := type <| ULift ℕ +@[expose] +def omega0 : OrderType := type <| ULift ℕ @[inherit_doc] scoped notation "ω" => OrderType.omega0 From 9ee99e66068ed9a8488a6542607a3aefd43e25aa Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Fri, 16 Jan 2026 22:52:59 +1100 Subject: [PATCH 06/13] Run `mk_all` --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3192355b35fd8c..b03bb3bfa59339 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5679,6 +5679,7 @@ public import Mathlib.Order.Synonym public import Mathlib.Order.TeichmullerTukey public import Mathlib.Order.TransfiniteIteration public import Mathlib.Order.TypeTags +public import Mathlib.Order.Types.Defs public import Mathlib.Order.ULift public import Mathlib.Order.UpperLower.Basic public import Mathlib.Order.UpperLower.Closure From ffbea393621fd06045c94efb3538f8e2457eb18d Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Sat, 17 Jan 2026 00:23:34 +1100 Subject: [PATCH 07/13] Add docs to instance Even though it is local and not exposed --- Mathlib/Order/Types/Defs.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 5a2605e1108677..06ccf6085d1d95 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -67,6 +67,8 @@ This is defined through the axiom of choice. -/ def ToType (o : OrderType) : Type u := o.out.carrier +/-- The local instance for some arbitrary linear order on `Type u` , order isomorphic within +order type `o`. -/ @[no_expose] local instance (o : OrderType) : LinearOrder o.ToType := o.out.str From 36dfe7715dec9969d2bed1d4267b600706dbeaee Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Sun, 18 Jan 2026 16:42:11 +1100 Subject: [PATCH 08/13] Apply review suggestions --- Mathlib/Order/Types/Defs.lean | 47 ++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 06ccf6085d1d95..d29c74c3692d90 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -50,12 +50,12 @@ variable {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} /-- Equivalence relation on linear orders on arbitrary types in universe `u`, given by order isomorphism. -/ -instance OrderType.instSetoid : Setoid LinOrd where +def OrderType.instSetoid : Setoid LinOrd where r := fun lin_ord₁ lin_ord₂ ↦ Nonempty (lin_ord₁ ≃o lin_ord₂) iseqv := ⟨fun _ ↦ ⟨.refl _⟩, fun ⟨e⟩ ↦ ⟨e.symm⟩, fun ⟨e₁⟩ ⟨e₂⟩ ↦ ⟨e₁.trans e₂⟩⟩ /-- `OrderType.{u}` is the type of linear orders in `Type u`, up to order isomorphism. -/ -@[pp_with_univ, no_expose] +@[pp_with_univ] def OrderType : Type (u + 1) := Quotient OrderType.instSetoid @@ -63,57 +63,58 @@ namespace OrderType /-- A "canonical" type order-isomorphic to the order type `o`, living in the same universe. This is defined through the axiom of choice. -/ -@[no_expose] def ToType (o : OrderType) : Type u := o.out.carrier +def ToLinord (o : OrderType) : LinearOrder o.ToType := + o.out.str + /-- The local instance for some arbitrary linear order on `Type u` , order isomorphic within order type `o`. -/ -@[no_expose] -local instance (o : OrderType) : LinearOrder o.ToType := - o.out.str +instance (o : OrderType) : LinearOrder o.ToType := + o.ToLinord /-! ### Basic properties of the order type -/ /-- The order type of the linear order on `α`. -/ -@[no_expose] def type (α : Type u) [LinearOrder α] : OrderType := ⟦⟨α⟩⟧ -@[no_expose] instance : Zero OrderType where zero := type PEmpty -instance inhabited : Inhabited OrderType := +instance : Inhabited OrderType := ⟨0⟩ -@[no_expose] instance : One OrderType where one := type PUnit @[simp] theorem type_toType (o : OrderType) : type o.ToType = o := surjInv_eq Quot.exists_rep o -theorem type_eq {α β} [LinearOrder α] [LinearOrder β] : +theorem type_eq_type {α β : Type u} [LinearOrder α] [LinearOrder β] : type α = type β ↔ Nonempty (α ≃o β) := Quotient.eq' -theorem _root_.RelIso.orderType_eq {α β} [LinearOrder α] +theorem _root_.OrderIso.orderTypeType_congr {α β} [LinearOrder α] + [LinearOrder β] (h : α ≃o β) : type α = type β := + type_eq_type.2 ⟨h⟩ + +theorem type_congr {α β} [LinearOrder α] [LinearOrder β] (h : α ≃o β) : type α = type β := - type_eq.2 ⟨h⟩ + type_eq_type.2 ⟨h⟩ @[simp] theorem type_of_isEmpty [LinearOrder α] [IsEmpty α] : type α = 0 := - (OrderIso.ofIsEmpty α PEmpty).orderType_eq + type_congr <| .ofIsEmpty α PEmpty -@[simp] theorem type_eq_zero [LinearOrder α] : type α = 0 ↔ IsEmpty α := ⟨fun h ↦ - let ⟨s⟩ := type_eq.1 h + let ⟨s⟩ := type_eq_type.1 h s.toEquiv.isEmpty, @type_of_isEmpty α _⟩ -theorem type_ne_zero_iff [LinearOrder α] : type α ≠ 0 ↔ Nonempty α := by simp +theorem type_ne_zero_iff [LinearOrder α] : type α ≠ 0 ↔ Nonempty α := by simp [type_eq_zero] theorem type_ne_zero [LinearOrder α] [h : Nonempty α] : type α ≠ 0 := type_ne_zero_iff.2 h @@ -121,11 +122,11 @@ theorem type_ne_zero [LinearOrder α] [h : Nonempty α] : type α ≠ 0 := @[simp] theorem type_of_unique [LinearOrder α] [Nonempty α] [Subsingleton α] : type α = 1 := by cases nonempty_unique α - exact (OrderIso.ofUnique α _).orderType_eq + exact (OrderIso.ofUnique α _).orderTypeType_congr @[simp] theorem type_eq_one [LinearOrder α] : type α = 1 ↔ Nonempty (Unique α) := - ⟨fun h ↦ let ⟨s⟩ := type_eq.1 h; ⟨s.toEquiv.unique⟩, + ⟨fun h ↦ let ⟨s⟩ := type_eq_type.1 h; ⟨s.toEquiv.unique⟩, fun ⟨_⟩ ↦ type_of_unique⟩ @[simp] @@ -139,7 +140,7 @@ private theorem nonempty_toType_iff {o : OrderType} : Nonempty o.ToType ↔ o protected theorem one_ne_zero : (1 : OrderType) ≠ 0 := type_ne_zero -instance nontrivial : Nontrivial OrderType.{u} := +instance : Nontrivial OrderType.{u} := ⟨⟨1, 0, OrderType.one_ne_zero⟩⟩ /-- `Quotient.inductionOn` specialized to `OrderType`. -/ @@ -191,7 +192,7 @@ instance : Preorder OrderType where le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ -instance instNeZeroOne : NeZero (1 : OrderType) := +instance : NeZero (1 : OrderType) := ⟨OrderType.one_ne_zero⟩ theorem type_le_type_iff {α β} [LinearOrder α] @@ -204,7 +205,7 @@ theorem type_le_type {α β} theorem type_lt_type {α β} [LinearOrder α] [LinearOrder β] (h : α ↪o β) (hne : ¬(Nonempty (β ↪o α))) : type α < type β := - ⟨⟨h⟩,hne⟩ + ⟨⟨h⟩, hne⟩ alias _root_.OrderEmbedding.type_le_type := type_le_type @@ -212,7 +213,7 @@ alias _root_.OrderEmbedding.type_le_type := type_le_type protected theorem zero_le (o : OrderType) : 0 ≤ o := inductionOn o (fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type) -instance instOrdBot : OrderBot OrderType where +instance : OrderBot OrderType where bot := 0 bot_le := OrderType.zero_le From 4ef3d575ed716a0c5cd68decfe206cc66bd522ae Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Sun, 18 Jan 2026 16:46:18 +1100 Subject: [PATCH 09/13] One more suggestion --- Mathlib/Order/Types/Defs.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index d29c74c3692d90..2f1e3c19eedb67 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -137,11 +137,8 @@ private theorem isEmpty_toType_iff {o : OrderType} : IsEmpty o.ToType ↔ o = 0 private theorem nonempty_toType_iff {o : OrderType} : Nonempty o.ToType ↔ o ≠ 0 := by rw [← @type_ne_zero_iff o.ToType, type_toType] -protected theorem one_ne_zero : (1 : OrderType) ≠ 0 := - type_ne_zero - instance : Nontrivial OrderType.{u} := - ⟨⟨1, 0, OrderType.one_ne_zero⟩⟩ + ⟨⟨1, 0, type_ne_zero⟩⟩ /-- `Quotient.inductionOn` specialized to `OrderType`. -/ @[elab_as_elim] @@ -193,7 +190,7 @@ instance : Preorder OrderType where le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ instance : NeZero (1 : OrderType) := - ⟨OrderType.one_ne_zero⟩ + ⟨type_ne_zero⟩ theorem type_le_type_iff {α β} [LinearOrder α] [LinearOrder β] : type α ≤ type β ↔ Nonempty (α ↪o β) := From a981b24c9b3b3eba6cf7beed0ff09686889dd6ff Mon Sep 17 00:00:00 2001 From: Yan Yablonovskiy Date: Sun, 18 Jan 2026 18:05:55 +1100 Subject: [PATCH 10/13] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Types/Defs.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 2f1e3c19eedb67..a615154ee26687 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -186,7 +186,7 @@ instance : Preorder OrderType where fun _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ propext ⟨fun ⟨h⟩ ↦ ⟨(f.symm.toOrderEmbedding.trans h).trans g.toOrderEmbedding⟩, fun ⟨h⟩ ↦ ⟨(f.toOrderEmbedding.trans h).trans g.symm.toOrderEmbedding⟩⟩ - le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) + le_refl o := inductionOn o fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩ le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ instance : NeZero (1 : OrderType) := @@ -208,7 +208,7 @@ alias _root_.OrderEmbedding.type_le_type := type_le_type @[simp] protected theorem zero_le (o : OrderType) : 0 ≤ o := - inductionOn o (fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type) + inductionOn o fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type instance : OrderBot OrderType where bot := 0 @@ -219,15 +219,15 @@ theorem bot_eq_zero : (⊥ : OrderType) = 0 := rfl @[simp] -protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := +protected theorem not_lt_zero {o : OrderType} : ¬o < 0 := not_lt_bot @[simp] theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := ⟨ne_bot_of_gt, fun ho ↦ by - convert type_lt_type (α := PEmpty) (β := o.ToType) ⟨Function.Embedding.ofIsEmpty, by simp⟩ - (fun ⟨f⟩ ↦ PEmpty.elim (f (Classical.choice (OrderType.nonempty_toType_iff.mpr ho)))) - simp⟩ + have := nonempty_toType_iff.2 ho + rw [← type_toType o] + exact ⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩⟩ /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ -- TODO: define `OrderType.lift` and redefine this using it. From 9b8172d368fa27c4cb690ddb2529744463f20691 Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Sun, 18 Jan 2026 18:48:28 +1100 Subject: [PATCH 11/13] Update Defs.lean --- Mathlib/Order/Types/Defs.lean | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index a615154ee26687..3b877e715cf9c1 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -66,13 +66,11 @@ This is defined through the axiom of choice. -/ def ToType (o : OrderType) : Type u := o.out.carrier -def ToLinord (o : OrderType) : LinearOrder o.ToType := - o.out.str - /-- The local instance for some arbitrary linear order on `Type u` , order isomorphic within order type `o`. -/ +@[no_expose] instance (o : OrderType) : LinearOrder o.ToType := - o.ToLinord + o.out.str /-! ### Basic properties of the order type -/ @@ -96,14 +94,12 @@ theorem type_eq_type {α β : Type u} [LinearOrder α] [LinearOrder β] : type α = type β ↔ Nonempty (α ≃o β) := Quotient.eq' -theorem _root_.OrderIso.orderTypeType_congr {α β} [LinearOrder α] - [LinearOrder β] (h : α ≃o β) : type α = type β := - type_eq_type.2 ⟨h⟩ - theorem type_congr {α β} [LinearOrder α] [LinearOrder β] (h : α ≃o β) : type α = type β := type_eq_type.2 ⟨h⟩ +alias _root_.OrderIso.type_congr := type_congr + @[simp] theorem type_of_isEmpty [LinearOrder α] [IsEmpty α] : type α = 0 := type_congr <| .ofIsEmpty α PEmpty @@ -122,7 +118,7 @@ theorem type_ne_zero [LinearOrder α] [h : Nonempty α] : type α ≠ 0 := @[simp] theorem type_of_unique [LinearOrder α] [Nonempty α] [Subsingleton α] : type α = 1 := by cases nonempty_unique α - exact (OrderIso.ofUnique α _).orderTypeType_congr + exact (OrderIso.ofUnique α _).type_congr @[simp] theorem type_eq_one [LinearOrder α] : type α = 1 ↔ Nonempty (Unique α) := @@ -186,7 +182,7 @@ instance : Preorder OrderType where fun _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ propext ⟨fun ⟨h⟩ ↦ ⟨(f.symm.toOrderEmbedding.trans h).trans g.toOrderEmbedding⟩, fun ⟨h⟩ ↦ ⟨(f.toOrderEmbedding.trans h).trans g.symm.toOrderEmbedding⟩⟩ - le_refl o := inductionOn o fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩ + le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ instance : NeZero (1 : OrderType) := @@ -201,14 +197,14 @@ theorem type_le_type {α β} ⟨h⟩ theorem type_lt_type {α β} - [LinearOrder α] [LinearOrder β] (h : α ↪o β) (hne : ¬(Nonempty (β ↪o α))) : type α < type β := - ⟨⟨h⟩, hne⟩ + [LinearOrder α] [LinearOrder β] (h : α ↪o β) (hne : IsEmpty (β ↪o α)) : type α < type β := + ⟨⟨h⟩, not_nonempty_iff.mpr hne⟩ alias _root_.OrderEmbedding.type_le_type := type_le_type @[simp] protected theorem zero_le (o : OrderType) : 0 ≤ o := - inductionOn o fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type + inductionOn o (fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type) instance : OrderBot OrderType where bot := 0 @@ -219,15 +215,18 @@ theorem bot_eq_zero : (⊥ : OrderType) = 0 := rfl @[simp] -protected theorem not_lt_zero {o : OrderType} : ¬o < 0 := +protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := not_lt_bot @[simp] -theorem pos_iff_ne_zero (o : OrderType) : 0 < o ↔ o ≠ 0 := - ⟨ne_bot_of_gt, fun ho ↦ by +theorem pos_iff_ne_zero {o : OrderType} : 0 < o ↔ o ≠ 0 where + mp := ne_bot_of_gt + mpr ho := by have := nonempty_toType_iff.2 ho rw [← type_toType o] - exact ⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩⟩ + exact ⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩ + + /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ -- TODO: define `OrderType.lift` and redefine this using it. From 4e287b48f353603ffe637db8963004b8fb9d30e9 Mon Sep 17 00:00:00 2001 From: YanYablonovskiy Date: Sun, 18 Jan 2026 18:52:34 +1100 Subject: [PATCH 12/13] Remove spurious spacing --- Mathlib/Order/Types/Defs.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 3b877e715cf9c1..643517ec7c5863 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -226,8 +226,6 @@ theorem pos_iff_ne_zero {o : OrderType} : 0 < o ↔ o ≠ 0 where rw [← type_toType o] exact ⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩ - - /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/ -- TODO: define `OrderType.lift` and redefine this using it. @[expose] From f08a940a7158b39ddac61d970d85c2e9f42e0023 Mon Sep 17 00:00:00 2001 From: Yan Yablonovskiy Date: Sun, 18 Jan 2026 19:13:58 +1100 Subject: [PATCH 13/13] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Types/Defs.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Order/Types/Defs.lean b/Mathlib/Order/Types/Defs.lean index 643517ec7c5863..10f9045c528ce1 100644 --- a/Mathlib/Order/Types/Defs.lean +++ b/Mathlib/Order/Types/Defs.lean @@ -182,7 +182,7 @@ instance : Preorder OrderType where fun _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ propext ⟨fun ⟨h⟩ ↦ ⟨(f.symm.toOrderEmbedding.trans h).trans g.toOrderEmbedding⟩, fun ⟨h⟩ ↦ ⟨(f.toOrderEmbedding.trans h).trans g.symm.toOrderEmbedding⟩⟩ - le_refl o := inductionOn o (fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩) + le_refl o := inductionOn o fun α _ ↦ ⟨(OrderIso.refl _).toOrderEmbedding⟩ le_trans o₁ o₂ o₃ := inductionOn₃ o₁ o₂ o₃ fun _ _ _ _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩ instance : NeZero (1 : OrderType) := @@ -204,7 +204,7 @@ alias _root_.OrderEmbedding.type_le_type := type_le_type @[simp] protected theorem zero_le (o : OrderType) : 0 ≤ o := - inductionOn o (fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type) + inductionOn o fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type instance : OrderBot OrderType where bot := 0 @@ -215,7 +215,7 @@ theorem bot_eq_zero : (⊥ : OrderType) = 0 := rfl @[simp] -protected theorem not_lt_zero (o : OrderType) : ¬o < 0 := +protected theorem not_lt_zero {o : OrderType} : ¬o < 0 := not_lt_bot @[simp]