Order types

Order types are defined as the quotient of linear orders under order isomorphism. They are preordered by order embeddings.

Main definitions

• 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 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

• https://en.wikipedia.org/wiki/Order_type
• 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

def OrderType.instSetoid : Setoid LinOrd

Equivalence relation on linear orders on arbitrary types in universe u, given by order isomorphism.

Equations

• OrderType.instSetoid = { r := fun (lin_ord₁ lin_ord₂ : LinOrd) => Nonempty (↑lin_ord₁ ≃o ↑lin_ord₂), iseqv := OrderType.instSetoid._proof_1✝ }

def OrderType : Type (u + 1)

OrderType.{u} is the type of linear orders in Type u, up to order isomorphism.

Equations

• OrderType.{?u.3} = Quotient OrderType.instSetoid

def OrderType.ToType (o : OrderType.{u}) : Type u

A "canonical" type order-isomorphic to the order type o, living in the same universe. This is defined through the axiom of choice.

Equations

• o.ToType = ↑(Quotient.out o)

@[instance_reducible]

instance OrderType.instLinearOrderToType (o : OrderType.{u_1}) : LinearOrder o.ToType

The instance for some arbitrary linear order on Type u , order isomorphic within order type o.

Equations

• o.instLinearOrderToType = (Quotient.out o).str

Basic properties of the order type

def OrderType.type (α : Type u) [LinearOrder α] : OrderType.{u}

The order type of the linear order on α.

Equations

• OrderType.type α = ⟦{ carrier := α, str := inst✝ }⟧

@[instance_reducible]

instance OrderType.instZero : Zero OrderType.{u_1}

Equations

• OrderType.instZero = { zero := OrderType.type PEmpty.{?u.3 + 1} }

@[instance_reducible]

instance OrderType.instInhabited : Inhabited OrderType.{u_1}

Equations

• OrderType.instInhabited = { default := 0 }

@[instance_reducible]

instance OrderType.instOne : One OrderType.{u_1}

Equations

• OrderType.instOne = { one := OrderType.type PUnit.{?u.3 + 1} }

@[simp]

theorem OrderType.type_toType (o : OrderType.{u_1}) : type o.ToType = o

theorem OrderType.type_eq_type {α β : Type u} [LinearOrder α] [LinearOrder β] : type α = type β ↔ Nonempty (α ≃o β)

theorem OrderType.type_congr {α β : Type u} [LinearOrder α] [LinearOrder β] (h : α ≃o β) : type α = type β

theorem OrderIso.type_congr {α β : Type u} [LinearOrder α] [LinearOrder β] (h : α ≃o β) : OrderType.type α = OrderType.type β

Alias of OrderType.type_congr.

@[simp]

theorem OrderType.type_of_isEmpty {α : Type u} [LinearOrder α] [IsEmpty α] : type α = 0

theorem OrderType.type_eq_zero {α : Type u} [LinearOrder α] : type α = 0 ↔ IsEmpty α

theorem OrderType.type_ne_zero_iff {α : Type u} [LinearOrder α] : type α ≠ 0 ↔ Nonempty α

@[simp]

theorem OrderType.type_ne_zero {α : Type u} [LinearOrder α] [h : Nonempty α] : type α ≠ 0

@[simp]

theorem OrderType.type_of_unique {α : Type u} [LinearOrder α] [Nonempty α] [Subsingleton α] : type α = 1

theorem OrderType.type_eq_one {α : Type u} [LinearOrder α] : type α = 1 ↔ Nonempty (Unique α)

instance OrderType.instNontrivial : Nontrivial OrderType.{u}

theorem OrderType.inductionOn {C : OrderType.{u_1} → Prop} (o : OrderType.{u_1}) (H : ∀ (α : Type u_1) [inst : LinearOrder α], C (type α)) : C o

Quotient.inductionOn specialized to OrderType.

theorem OrderType.inductionOn₂ {C : OrderType.{u_1} → OrderType.{u_2} → Prop} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2}) (H : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β], C (type α) (type β)) : C o₁ o₂

Quotient.inductionOn₂ specialized to OrderType.

theorem OrderType.inductionOn₃ {C : OrderType.{u_1} → OrderType.{u_2} → OrderType.{u_3} → Prop} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2}) (o₃ : OrderType.{u_3}) (H : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β] (γ : Type u_3) [inst_2 : LinearOrder γ], C (type α) (type β) (type γ)) : C o₁ o₂ o₃

Quotient.inductionOn₃ specialized to OrderType.

def OrderType.liftOn {δ : Sort v} (o : OrderType.{u_1}) (f : (α : Type u_1) → [LinearOrder α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β], type α = type β → f α = f β) : δ

To define a function on OrderType, it suffices to define it on all linear orders.

Equations

• o.liftOn f c = Quotient.liftOn o (fun (w : LinOrd) => f ↑w) ⋯

def OrderType.liftOn₂ {δ : Sort v} (o₁ : OrderType.{u_1}) (o₂ : OrderType.{u_2}) (f : (α : Type u_1) → [LinearOrder α] → (β : Type u_2) → [LinearOrder β] → δ) (c : ∀ (α₁ : Type u_1) [inst : LinearOrder α₁] (β₁ : Type u_2) [inst_1 : LinearOrder β₁] (α₂ : Type u_1) [inst_2 : LinearOrder α₂] (β₂ : Type u_2) [inst_3 : LinearOrder β₂], type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂) : δ

Quotient.liftOn₂ specialized to OrderType.

Equations

• o₁.liftOn₂ o₂ f c = Quotient.liftOn₂ o₁ o₂ (fun (w : LinOrd) (v : LinOrd) => f ↑w ↑v) ⋯

@[simp]

theorem OrderType.liftOn_type {δ : Sort v} (f : (α : Type u_1) → [LinearOrder α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β], type α = type β → f α = f β) {γ : Type u_1} [LinearOrder γ] : (type γ).liftOn f c = f γ

@[simp]

theorem OrderType.liftOn₂_type {α : Type u} {β : Type v} {δ : Type u_1} [LinearOrder α] [LinearOrder β] (f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ) (c : ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_1 : LinearOrder β₁] (α₂ : Type u) [inst_2 : LinearOrder α₂] (β₂ : Type v) [inst_3 : LinearOrder β₂], type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂) : (type α).liftOn₂ (type β) f c = f α β

The order on OrderType

@[instance_reducible]

instance OrderType.instPreorder : Preorder OrderType.{u_1}

The order is defined so that type α ≤ type β iff there exists an order embedding α ↪o β.

Equations

• One or more equations did not get rendered due to their size.

instance OrderType.instNeZeroOfNat : NeZero 1

theorem OrderType.type_le_type_iff {α β : Type u} [LinearOrder α] [LinearOrder β] : type α ≤ type β ↔ Nonempty (α ↪o β)

theorem OrderType.type_le_type {α β : Type u} [LinearOrder α] [LinearOrder β] (h : α ↪o β) : type α ≤ type β

theorem OrderType.type_lt_type {α β : Type u} [LinearOrder α] [LinearOrder β] (h : α ↪o β) (hne : IsEmpty (β ↪o α)) : type α < type β

theorem OrderEmbedding.type_le_type {α β : Type u} [LinearOrder α] [LinearOrder β] (h : α ↪o β) : OrderType.type α ≤ OrderType.type β

Alias of OrderType.type_le_type.

@[simp]

theorem OrderType.zero_le (o : OrderType.{u_1}) : 0 ≤ o

@[instance_reducible]

instance OrderType.instOrderBot : OrderBot OrderType.{u_1}

Equations

• OrderType.instOrderBot = { bot := 0, bot_le := OrderType.zero_le }

@[simp]

theorem OrderType.bot_eq_zero : ⊥ = 0

@[simp]

theorem OrderType.not_lt_zero {o : OrderType.{u_1}} : ¬o < 0

@[simp]

theorem OrderType.pos_iff_ne_zero {o : OrderType.{u_1}} : 0 < o ↔ o ≠ 0

def OrderType.omega0 : OrderType.{u_1}

ω is the first infinite ordinal, defined as the order type of ℕ.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega0.

Equations

• OrderType.omega0 = OrderType.type (ULift.{?u.3, 0} ℕ)

def OrderType.termω : Lean.ParserDescr

ω is the first infinite ordinal, defined as the order type of ℕ.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega0.

Equations

• OrderType.termω = Lean.ParserDescr.node `OrderType.termω 1024 (Lean.ParserDescr.symbol "ω")

@[simp]

theorem OrderType.type_nat : type ℕ = omega0