Ordinals

Ordinals are defined as equivalences of well-ordered sets under order isomorphism. They are endowed with a total order, where an ordinal is smaller than another one if it embeds into it as an initial segment (or, equivalently, in any way). This total order is well founded.

Main definitions

• Ordinal: the type of ordinals (in a given universe)

• Ordinal.type r: given a well-founded order r, this is the corresponding ordinal

• Ordinal.typein r a: given a well-founded order r on a type α, and a : α, the ordinal corresponding to all elements smaller than a.

• enum r ⟨o, h⟩: given a well-order r on a type α, and an ordinal o strictly smaller than the ordinal corresponding to r (this is the assumption h), returns the o-th element of α. In other words, the elements of α can be enumerated using ordinals up to type r.

• Ordinal.card o: the cardinality of an ordinal o.

• Ordinal.lift lifts an ordinal in universe u to an ordinal in universe max u v. For a version registering additionally that this is an initial segment embedding, see Ordinal.liftInitialSeg. For a version registering that it is a principal segment embedding if u < v, see Ordinal.liftPrincipalSeg.

• Ordinal.omega0 or ω is the order type of ℕ. It is called this to match Cardinal.aleph0 and so that the omega function can be named Ordinal.omega. This definition is universe polymorphic: Ordinal.omega0.{u} : Ordinal.{u} (contrast with ℕ : Type, which lives in a specific universe). In some cases the universe level has to be given explicitly.

• o₁ + o₂ is the order on the disjoint union of o₁ and o₂ obtained by declaring that every element of o₁ is smaller than every element of o₂. The main properties of addition (and the other operations on ordinals) are stated and proved in Mathlib/SetTheory/Ordinal/Arithmetic.lean. Here, we only introduce it and prove its basic properties to deduce the fact that the order on ordinals is total (and well founded).

• succ o is the successor of the ordinal o.

• Cardinal.ord c: when c is a cardinal, ord c is the smallest ordinal with this cardinality. It is the canonical way to represent a cardinal with an ordinal.

A conditionally complete linear order with bot structure is registered on ordinals, where ⊥ is 0, the ordinal corresponding to the empty type, and Inf is the minimum for nonempty sets and 0 for the empty set by convention.

Notation

• ω is a notation for the first infinite ordinal in the scope Ordinal.

Definition of ordinals

structure WellOrder : Type (u + 1)

Bundled structure registering a well order on a type. Ordinals will be defined as a quotient of this type.

• α : Type u

  The underlying type of the order.

• r : self.α → self.α → Prop

  The underlying relation of the order.

• wo : IsWellOrder self.α self.r

  The proposition that r is a well-ordering for α.

@[implicit_reducible]

instance WellOrder.inhabited : Inhabited WellOrder

@[implicit_reducible]

instance Ordinal.isEquivalent : Setoid WellOrder

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

def Ordinal : Type (u + 1)

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

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

A "canonical" type order-isomorphic to the ordinal o, living in the same universe. This is defined through the axiom of choice; in particular, it has no useful def-eqs, and it is not exposed.

Use this over Iio o only when it is paramount to have a Type u rather than a Type (u + 1), and convert using

Ordinal.ToType.mk : Iio o → o.ToType
Ordinal.ToType.toOrd : o.ToType → Iio o

@[deprecated Ordinal.ToType (since := "2025-12-04")]

def Ordinal.toType (o : Ordinal.{u}) : Type u

Alias of Ordinal.ToType.

---

A "canonical" type order-isomorphic to the ordinal o, living in the same universe. This is defined through the axiom of choice; in particular, it has no useful def-eqs, and it is not exposed.

Use this over Iio o only when it is paramount to have a Type u rather than a Type (u + 1), and convert using

Ordinal.ToType.mk : Iio o → o.ToType
Ordinal.ToType.toOrd : o.ToType → Iio o

@[implicit_reducible]

noncomputable instance linearOrder_toType (o : Ordinal.{u_1}) : LinearOrder o.ToType

instance wellFoundedLT_toType (o : Ordinal.{u_1}) : WellFoundedLT o.ToType

@[implicit_reducible]

noncomputable instance hasWellFounded_toType (o : Ordinal.{u_1}) : WellFoundedRelation o.ToType

@[implicit_reducible]

noncomputable instance Ordinal.instSuccOrderToType (o : Ordinal.{u_1}) : SuccOrder o.ToType

Basic properties of the order type

def Ordinal.type {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal.{u}

The order type of a well order is an ordinal.

def Ordinal.termTypeLT_ : Lean.ParserDescr

typeLT α is an abbreviation for the order type of the < relation of α.

@[implicit_reducible]

instance Ordinal.zero : Zero Ordinal.{u_1}

@[implicit_reducible]

instance Ordinal.inhabited : Inhabited Ordinal.{u_1}

@[implicit_reducible]

instance Ordinal.one : One Ordinal.{u_1}

@[simp]

theorem Ordinal.type_toType (o : Ordinal.{u_1}) : (type fun (x1 x2 : o.ToType) => x1 < x2) = o

theorem Ordinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : type r = type s ↔ Nonempty (r ≃r s)

theorem RelIso.ordinal_type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) : Ordinal.type r = Ordinal.type s

theorem Ordinal.type_eq_zero_of_empty {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [IsEmpty α] : type r = 0

@[simp]

theorem Ordinal.type_eq_zero_iff_isEmpty {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : type r = 0 ↔ IsEmpty α

theorem Ordinal.type_ne_zero_iff_nonempty {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : type r ≠ 0 ↔ Nonempty α

theorem Ordinal.type_ne_zero_of_nonempty {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [h : Nonempty α] : type r ≠ 0

theorem Ordinal.type_pEmpty : type emptyRelation = 0

theorem Ordinal.type_empty : type emptyRelation = 0

theorem Ordinal.type_eq_one_of_unique {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [Nonempty α] [Subsingleton α] : type r = 1

@[simp]

theorem Ordinal.type_eq_one_iff_unique {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : type r = 1 ↔ Nonempty (Unique α)

theorem Ordinal.type_pUnit : type emptyRelation = 1

theorem Ordinal.type_unit : type emptyRelation = 1

@[simp]

theorem Ordinal.isEmpty_toType_iff {o : Ordinal.{u_1}} : IsEmpty o.ToType ↔ o = 0

@[deprecated Ordinal.isEmpty_toType_iff (since := "2026-02-18")]

theorem Ordinal.toType_empty_iff_eq_zero {o : Ordinal.{u_1}} : IsEmpty o.ToType ↔ o = 0

Alias of Ordinal.isEmpty_toType_iff.

instance Ordinal.isEmpty_toType_zero : IsEmpty (ToType 0)

@[simp]

theorem Ordinal.nonempty_toType_iff {o : Ordinal.{u_1}} : Nonempty o.ToType ↔ o ≠ 0

@[deprecated Ordinal.nonempty_toType_iff (since := "2026-02-18")]

theorem Ordinal.toType_nonempty_iff_ne_zero {o : Ordinal.{u_1}} : Nonempty o.ToType ↔ o ≠ 0

Alias of Ordinal.nonempty_toType_iff.

theorem Ordinal.one_ne_zero : 1 ≠ 0

instance Ordinal.nontrivial : Nontrivial Ordinal.{u}

theorem Ordinal.inductionOn {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r], motive (type r)) : motive o

Quotient.inductionOn specialized to ordinals.

Not to be confused with well-founded induction WellFoundedLT.induction.

theorem Ordinal.inductionOn₂ {motive : Ordinal.{u_1} → Ordinal.{u_2} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop) [inst_1 : IsWellOrder β s], motive (type r) (type s)) : motive o₁ o₂

Quotient.inductionOn₂ specialized to ordinals.

Not to be confused with well-founded induction WellFoundedLT.induction.

theorem Ordinal.inductionOn₃ {motive : Ordinal.{u_1} → Ordinal.{u_2} → Ordinal.{u_3} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}) (o₃ : Ordinal.{u_3}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop) [inst_1 : IsWellOrder β s] (γ : Type u_3) (t : γ → γ → Prop) [inst_2 : IsWellOrder γ t], motive (type r) (type s) (type t)) : motive o₁ o₂ o₃

Quotient.inductionOn₃ specialized to ordinals.

Not to be confused with well-founded induction WellFoundedLT.induction.

theorem Ordinal.inductionOnWellOrder {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}) (type : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], motive (type fun (x1 x2 : α) => x1 < x2)) : motive o

To prove a result on ordinals, it suffices to prove it for order types of well-orders.

noncomputable def Ordinal.liftOnWellOrder {δ : Sort v} (o : Ordinal.{u_1}) (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β] [inst_3 : WellFoundedLT β], ((type fun (x1 x2 : α) => x1 < x2) = type fun (x1 x2 : β) => x1 < x2) → f α = f β) : δ

To define a function on ordinals, it suffices to define them on order types of well-orders.

Since LinearOrder is data-carrying, liftOnWellOrder_type is not a definitional equality, unlike Quotient.liftOn_mk which is always def-eq.

@[simp]

theorem Ordinal.liftOnWellOrder_type {δ : Sort v} (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β] [inst_3 : WellFoundedLT β], ((type fun (x1 x2 : α) => x1 < x2) = type fun (x1 x2 : β) => x1 < x2) → f α = f β) {γ : Type u_1} [LinearOrder γ] [WellFoundedLT γ] : (type fun (x1 x2 : γ) => x1 < x2).liftOnWellOrder f c = f γ

The order on ordinals

@[implicit_reducible]

instance Ordinal.partialOrder : PartialOrder Ordinal.{u_1}

For Ordinal:

• less-equal is defined such that well orders r and s satisfy type r ≤ type s if there exists a function embedding r as an initial segment of s.
• less-than is defined such that well orders r and s satisfy type r < type s if there exists a function embedding r as a principal segment of s.

Note that most of the relevant results on initial and principal segments are proved in the Mathlib/Order/InitialSeg.lean file.

@[implicit_reducible]

noncomputable instance Ordinal.instLinearOrder : LinearOrder Ordinal.{u_1}

theorem InitialSeg.ordinal_type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : InitialSeg r s) : Ordinal.type r ≤ Ordinal.type s

theorem RelEmbedding.ordinal_type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ↪r s) : Ordinal.type r ≤ Ordinal.type s

theorem PrincipalSeg.ordinal_type_lt {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : PrincipalSeg r s) : Ordinal.type r < Ordinal.type s

@[implicit_reducible]

instance Ordinal.instOrderBot : OrderBot Ordinal.{u_1}

@[simp]

theorem Ordinal.bot_eq_zero : ⊥ = 0

instance Ordinal.instIsEmptyIioZero : IsEmpty ↑(Set.Iio 0)

@[deprecated nonpos_iff_eq_zero (since := "2025-11-21")]

theorem Ordinal.le_zero {o : Ordinal.{u_1}} : o ≤ 0 ↔ o = 0

@[deprecated not_neg (since := "2025-11-21")]

theorem Ordinal.not_lt_zero (o : Ordinal.{u_1}) : ¬o < 0

@[deprecated eq_zero_or_pos (since := "2025-11-21")]

theorem Ordinal.eq_zero_or_pos (a : Ordinal.{u_1}) : a = 0 ∨ 0 < a

instance Ordinal.instZeroLEOneClass : ZeroLEOneClass Ordinal.{u_1}

instance Ordinal.instNeZeroOne : NeZero 1

theorem Ordinal.type_le_iff {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : type r ≤ type s ↔ Nonempty (InitialSeg r s)

theorem Ordinal.type_le_iff' {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : type r ≤ type s ↔ Nonempty (r ↪r s)

theorem Ordinal.type_lt_iff {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : type r < type s ↔ Nonempty (PrincipalSeg r s)

noncomputable def Ordinal.initialSegToType {α β : Ordinal.{u_1}} (h : α ≤ β) : InitialSeg (fun (x1 x2 : α.ToType) => x1 < x2) fun (x1 x2 : β.ToType) => x1 < x2

Given two ordinals α ≤ β, then initialSegToType α β is the initial segment embedding of α.ToType into β.ToType.

noncomputable def Ordinal.principalSegToType {α β : Ordinal.{u_1}} (h : α < β) : PrincipalSeg (fun (x1 x2 : α.ToType) => x1 < x2) fun (x1 x2 : β.ToType) => x1 < x2

Given two ordinals α < β, then principalSegToType α β is the principal segment embedding of α.ToType into β.ToType.

Enumerating elements in a well-order with ordinals

def Ordinal.typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : PrincipalSeg r fun (x1 x2 : Ordinal.{u}) => x1 < x2

The order type of an element inside a well order.

This is registered as a principal segment embedding into the ordinals, with top type r.

@[simp]

theorem Ordinal.type_subrel {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : type (Subrel r fun (x : α) => r x a) = (typein r).toRelEmbedding a

@[simp]

theorem Ordinal.top_typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (typein r).top = type r

theorem Ordinal.typein_lt_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : (typein r).toRelEmbedding a < type r

theorem Ordinal.typein_lt_self {o : Ordinal.{u_1}} (i : o.ToType) : (typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding i < o

@[simp]

theorem Ordinal.typein_top {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg r s) : (typein s).toRelEmbedding f.top = type r

@[simp]

theorem Ordinal.typein_lt_typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {a b : α} : (typein r).toRelEmbedding a < (typein r).toRelEmbedding b ↔ r a b

@[simp]

theorem Ordinal.typein_le_typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {a b : α} : (typein r).toRelEmbedding a ≤ (typein r).toRelEmbedding b ↔ ¬r b a

theorem Ordinal.typein_injective {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : Function.Injective ⇑(typein r).toRelEmbedding

theorem Ordinal.typein_inj {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {a b : α} : (typein r).toRelEmbedding a = (typein r).toRelEmbedding b ↔ a = b

theorem Ordinal.mem_range_typein_iff {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} : o ∈ Set.range ⇑(typein r).toRelEmbedding ↔ o < type r

theorem Ordinal.typein_surj {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < type r) : o ∈ Set.range ⇑(typein r).toRelEmbedding

theorem Ordinal.typein_surjOn {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : Set.SurjOn (⇑(typein r).toRelEmbedding) Set.univ (Set.Iio (type r))

@[simp]

theorem Ordinal.type_Iio_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] (x : α) : type LT.lt = (typein LT.lt).toRelEmbedding x

noncomputable def Ordinal.enum {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (fun (x1 x2 : ↑(Set.Iio (type r))) => x1 < x2) ≃r r

A well order r is order-isomorphic to the set of ordinals smaller than type r. enum r ⟨o, h⟩ is the o-th element of α ordered by r.

That is, enum maps an initial segment of the ordinals, those less than the order type of r, to the elements of α.

@[simp]

theorem Ordinal.enum_symm_apply_coe {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a✝ : α) : ↑((enum r).symm a✝) = (typein r).toRelEmbedding a✝

@[simp]

theorem Ordinal.typein_enum {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < type r) : (typein r).toRelEmbedding ((enum r) ⟨o, h⟩) = o

theorem Ordinal.enum_type {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg s r) {h : type s < type r} : (enum r) ⟨type s, h⟩ = f.top

@[simp]

theorem Ordinal.enum_typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : (enum r) ⟨(typein r).toRelEmbedding a, ⋯⟩ = a

theorem Ordinal.enum_lt_enum {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (type r))} : r ((enum r) o₁) ((enum r) o₂) ↔ o₁ < o₂

theorem Ordinal.enum_le_enum {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (type r))} : ¬r ((enum r) o₁) ((enum r) o₂) ↔ o₂ ≤ o₁

@[simp]

theorem Ordinal.enum_le_enum' (a : Ordinal.{u_1}) {o₁ o₂ : ↑(Set.Iio (type fun (x1 x2 : a.ToType) => x1 < x2))} : (enum fun (x1 x2 : a.ToType) => x1 < x2) o₁ ≤ (enum fun (x1 x2 : a.ToType) => x1 < x2) o₂ ↔ o₁ ≤ o₂

theorem Ordinal.enum_inj {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (type r))} : (enum r) o₁ = (enum r) o₂ ↔ o₁ = o₂

theorem Ordinal.enum_zero_le {α : Type u} {r : α → α → Prop} [IsWellOrder α r] (h0 : 0 < type r) (a : α) : ¬r a ((enum r) ⟨0, h0⟩)

theorem Ordinal.enum_zero_le' {o : Ordinal.{u_1}} (h0 : 0 < o) (a : o.ToType) : (enum fun (x1 x2 : o.ToType) => x1 < x2) ⟨0, ⋯⟩ ≤ a

theorem Ordinal.relIso_enum' {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < type r) (hs : o < type s) : f ((enum r) ⟨o, hr⟩) = (enum s) ⟨o, hs⟩

theorem Ordinal.relIso_enum {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < type r) : f ((enum r) ⟨o, hr⟩) = (enum s) ⟨o, ⋯⟩

noncomputable def Ordinal.ToType.mk {o : Ordinal.{u_1}} : ↑(Set.Iio o) ≃o o.ToType

The order isomorphism between ordinals less than o and o.ToType.

theorem Ordinal.ToType.mk_symm_apply_coe {o : Ordinal.{u_1}} (x : o.ToType) : ↑((RelIso.symm mk) x) = (typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding x

theorem Ordinal.ToType.mk_apply {o : Ordinal.{u_1}} (x : ↑(Set.Iio o)) : mk x = (enum fun (x1 x2 : o.ToType) => x1 < x2) ⟨↑x, ⋯⟩

@[deprecated Ordinal.ToType.mk (since := "2025-12-04")]

def Ordinal.enumIsoToType {o : Ordinal.{u_1}} : ↑(Set.Iio o) ≃o o.ToType

Alias of Ordinal.ToType.mk.

---

The order isomorphism between ordinals less than o and o.ToType.

@[reducible, inline]

noncomputable abbrev Ordinal.ToType.toOrd {o : Ordinal.{u_1}} (α : o.ToType) : ↑(Set.Iio o)

Convert an element of α.toType to the corresponding Ordinal

@[implicit_reducible]

noncomputable instance Ordinal.instCoeToTypeElemIio (o : Ordinal.{u_1}) : Coe o.ToType ↑(Set.Iio o)

@[implicit_reducible]

noncomputable instance Ordinal.instCoeOutToType (o : Ordinal.{u_1}) : CoeOut o.ToType Ordinal.{u_1}

instance Ordinal.small_Iio (o : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Iio o)

instance Ordinal.small_Iic (o : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Iic o)

instance Ordinal.small_Ico (a b : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Ico a b)

instance Ordinal.small_Icc (a b : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Icc a b)

instance Ordinal.small_Ioo (a b : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Ioo a b)

instance Ordinal.small_Ioc (a b : Ordinal.{u}) : Small.{u, u + 1} ↑(Set.Ioc a b)

@[implicit_reducible]

noncomputable def Ordinal.toTypeOrderBot {o : Ordinal.{u_1}} (ho : o ≠ 0) : OrderBot o.ToType

o.ToType is an OrderBot whenever o ≠ 0.

theorem Ordinal.enum_zero_eq_bot {o : Ordinal.{u_1}} (ho : 0 < o) : (enum fun (x1 x2 : o.ToType) => x1 < x2) ⟨0, ⋯⟩ = have H := toTypeOrderBot ⋯; ⊥

theorem Ordinal.lt_wf : WellFounded fun (x1 x2 : Ordinal.{u_1}) => x1 < x2

@[implicit_reducible]

instance Ordinal.wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}

instance Ordinal.wellFoundedLT : WellFoundedLT Ordinal.{u_1}

@[implicit_reducible]

noncomputable instance Ordinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Ordinal.{u_1}

@[deprecated WellFoundedLT.induction (since := "2026-02-27")]

theorem Ordinal.induction {p : Ordinal.{u} → Prop} (i : Ordinal.{u}) (h : ∀ (j : Ordinal.{u}), (∀ k < j, p k) → p j) : p i

theorem Ordinal.typein_apply {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : InitialSeg r s) (a : α) : (typein s).toRelEmbedding (f a) = (typein r).toRelEmbedding a

Cardinality of ordinals

def Ordinal.card : Ordinal.{u_1} → Cardinal.{u_1}

The cardinal of an ordinal is the cardinality of any type on which a relation with that order type is defined.

@[simp]

theorem Ordinal.card_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (type r).card = Cardinal.mk α

@[simp]

theorem Ordinal.card_typein {α : Type u} {r : α → α → Prop} [IsWellOrder α r] (x : α) : ((typein r).toRelEmbedding x).card = Cardinal.mk { y : α // r y x }

theorem Ordinal.card_le_card {o₁ o₂ : Ordinal.{u_1}} : o₁ ≤ o₂ → o₁.card ≤ o₂.card

@[simp]

theorem Ordinal.card_zero : card 0 = 0

@[simp]

theorem Ordinal.card_one : card 1 = 1

theorem Ordinal.card_typein_min_le_mk {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {s : Set α} (hs : sᶜ.Nonempty) : ((typein r).toRelEmbedding (⋯.min sᶜ hs)).card ≤ Cardinal.mk ↑s

The cardinality of a set is an upper-bound for the cardinality of the order type of the set's mex (minimum excluded value). See not_lt_enum_ord_mk_min_compl for the α version.

Lifting ordinals to a higher universe

def Ordinal.lift (o : Ordinal.{v}) : Ordinal.{max v u}

The universe lift operation for ordinals, which embeds Ordinal.{u} as a proper initial segment of Ordinal.{v} for v > u. For the initial segment version, see liftInitialSeg.

@[simp]

theorem Ordinal.type_ulift {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : type (ULift.down ⁻¹'o r) = lift.{v, u} (type r)

@[deprecated Ordinal.type_ulift (since := "2026-02-20")]

theorem Ordinal.type_uLift {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : type (ULift.down ⁻¹'o r) = lift.{v, u} (type r)

Alias of Ordinal.type_ulift.

@[simp]

theorem Ordinal.type_lt_ulift {α : Type u} [LinearOrder α] [WellFoundedLT α] : (type fun (x1 x2 : ULift.{v, u} α) => x1 < x2) = lift.{v, u} (type fun (x1 x2 : α) => x1 < x2)

theorem RelIso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) : Ordinal.lift.{v, u} (Ordinal.type r) = Ordinal.lift.{u, v} (Ordinal.type s)

@[simp]

theorem Ordinal.type_preimage {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : type (⇑f ⁻¹'o r) = type r

@[simp]

theorem Ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : lift.{u, v} (type (⇑f ⁻¹'o r)) = lift.{v, u} (type r)

theorem Ordinal.lift_umax : lift.{max u v, u} = lift.{v, u}

lift.{max u v, u} equals lift.{v, u}.

Unfortunately, the simp lemma doesn't seem to work.

theorem Ordinal.lift_id' (a : Ordinal.{max u_1 u_2}) : lift.{u_1, max u_1 u_2} a = a

An ordinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work.

@[simp]

theorem Ordinal.lift_id (a : Ordinal.{u}) : lift.{u, u} a = a

An ordinal lifted to the same universe equals itself.

@[simp]

theorem Ordinal.lift_uzero (a : Ordinal.{u}) : lift.{0, u} a = a

An ordinal lifted to the zero universe equals itself.

theorem Ordinal.lift_type_le {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (InitialSeg r s)

theorem Ordinal.lift_type_eq {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

theorem Ordinal.lift_type_lt {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (PrincipalSeg r s)

@[simp]

theorem Ordinal.lift_le {a b : Ordinal.{v}} : lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b

@[simp]

theorem Ordinal.lift_inj {a b : Ordinal.{v}} : lift.{u, v} a = lift.{u, v} b ↔ a = b

@[simp]

theorem Ordinal.lift_lt {a b : Ordinal.{v}} : lift.{u, v} a < lift.{u, v} b ↔ a < b

@[simp]

theorem Ordinal.lift_typein_top {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg r s) : lift.{u, v} ((typein s).toRelEmbedding f.top) = lift.{v, u} (type r)

def Ordinal.liftInitialSeg : InitialSeg (fun (x1 x2 : Ordinal.{v}) => x1 < x2) fun (x1 x2 : Ordinal.{max u v}) => x1 < x2

Initial segment version of the lift operation on ordinals, embedding Ordinal.{u} in Ordinal.{v} as an initial segment when u ≤ v.

@[simp]

theorem Ordinal.liftInitialSeg_coe : ⇑liftInitialSeg = lift.{v, u}

@[simp]

theorem Ordinal.lift_lift (a : Ordinal.{u}) : lift.{w, max v u} (lift.{v, u} a) = lift.{max v w, u} a

@[simp]

theorem Ordinal.lift_zero : lift.{u_2, u_1} 0 = 0

@[simp]

theorem Ordinal.lift_one : lift.{u_2, u_1} 1 = 1

@[simp]

theorem Ordinal.lift_card (a : Ordinal.{v}) : Cardinal.lift.{u, v} a.card = (lift.{u, v} a).card

theorem Ordinal.mem_range_lift_of_le {a : Ordinal.{u}} {b : Ordinal.{max u v}} (h : b ≤ lift.{v, u} a) : b ∈ Set.range lift.{v, u}

theorem Ordinal.le_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v}} : b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b

theorem Ordinal.lt_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v}} : b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b

The first infinite ordinal ω

def Ordinal.omega0 : Ordinal.{u}

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

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega0.

def Ordinal.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.

@[simp]

theorem Ordinal.type_nat_lt : (type fun (x1 x2 : ℕ) => x1 < x2) = omega0

Note that the presence of this lemma makes simp [omega0] form a loop.

@[simp]

theorem Ordinal.card_omega0 : omega0.card = Cardinal.aleph0

@[simp]

theorem Ordinal.lift_omega0 : lift.{u_1, u_2} omega0 = omega0

Definition and first properties of addition on ordinals

In this paragraph, we introduce the addition on ordinals, and prove just enough properties to deduce that the order on ordinals is total (and therefore well-founded). Further properties of the addition, together with properties of the other operations, are proved in Mathlib/SetTheory/Ordinal/Arithmetic.lean.

@[implicit_reducible]

instance Ordinal.add : Add Ordinal.{u}

o₁ + o₂ is the order on the disjoint union of o₁ and o₂ obtained by declaring that every element of o₁ is smaller than every element of o₂.

@[implicit_reducible]

instance Ordinal.addMonoidWithOne : AddMonoidWithOne Ordinal.{u}

@[simp]

theorem Ordinal.card_add (o₁ o₂ : Ordinal.{u_1}) : (o₁ + o₂).card = o₁.card + o₂.card

theorem Ordinal.card_add_one (o : Ordinal.{u_1}) : (o + 1).card = o.card + 1

@[simp]

theorem Ordinal.type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : type (Sum.Lex r s) = type r + type s

@[simp]

theorem Ordinal.card_nat (n : ℕ) : (↑n).card = ↑n

@[simp]

theorem Ordinal.card_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).card = OfNat.ofNat n

instance Ordinal.instAddLeftMono : AddLeftMono Ordinal.{u}

instance Ordinal.instAddRightMono : AddRightMono Ordinal.{u}

instance Ordinal.existsAddOfLE : ExistsAddOfLE Ordinal.{u_1}

instance Ordinal.canonicallyOrderedAdd : CanonicallyOrderedAdd Ordinal.{u_1}

@[deprecated le_self_add (since := "2025-11-21")]

theorem Ordinal.le_add_right (a b : Ordinal.{u_1}) : a ≤ a + b

@[deprecated le_add_self (since := "2025-11-21")]

theorem Ordinal.le_add_left (a b : Ordinal.{u_1}) : a ≤ b + a

theorem Ordinal.max_zero_left (a : Ordinal.{u_1}) : max 0 a = a

theorem Ordinal.max_zero_right (a : Ordinal.{u_1}) : max a 0 = a

@[simp]

theorem Ordinal.max_eq_zero {a b : Ordinal.{u_1}} : max a b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem Ordinal.sInf_empty : sInf ∅ = 0

Successor order properties

instance Ordinal.instNoMaxOrder : NoMaxOrder Ordinal.{u_1}

@[implicit_reducible]

instance Ordinal.instSuccOrder : SuccOrder Ordinal.{u}

@[implicit_reducible]

instance Ordinal.instSuccAddOrder : SuccAddOrder Ordinal.{u_1}

@[deprecated Order.succ_eq_add_one (since := "2026-02-26")]

theorem Ordinal.add_one_eq_succ (o : Ordinal.{u_1}) : o + 1 = Order.succ o

@[deprecated zero_add (since := "2026-02-26")]

theorem Ordinal.succ_zero : Order.succ 0 = 1

@[deprecated one_add_one_eq_two (since := "2026-02-26")]

theorem Ordinal.succ_one : Order.succ 1 = 2

@[deprecated add_assoc (since := "2026-02-26")]

theorem Ordinal.add_succ (o₁ o₂ : Ordinal.{u_1}) : o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)

@[deprecated Order.one_le_iff_ne_zero (since := "2026-03-24")]

theorem Ordinal.one_le_iff_ne_zero {o : Ordinal.{u_1}} : 1 ≤ o ↔ o ≠ 0

theorem Ordinal.succ_pos (o : Ordinal.{u_1}) : 0 < Order.succ o

theorem Ordinal.add_one_ne_zero (o : Ordinal.{u_1}) : o + 1 ≠ 0

@[deprecated Ordinal.add_one_ne_zero (since := "2026-02-27")]

theorem Ordinal.succ_ne_zero (o : Ordinal.{u_1}) : Order.succ o ≠ 0

@[deprecated Order.lt_one_iff (since := "2026-03-24")]

theorem Ordinal.lt_one_iff_zero {a : Ordinal.{u_1}} : a < 1 ↔ a = 0

@[deprecated Order.le_one_iff (since := "2026-03-24")]

theorem Ordinal.le_one_iff {a : Ordinal.{u_1}} : a ≤ 1 ↔ a = 0 ∨ a = 1

@[deprecated Ordinal.card_add_one (since := "2026-02-27")]

theorem Ordinal.card_succ (o : Ordinal.{u_1}) : (Order.succ o).card = o.card + 1

theorem Ordinal.natCast_succ (n : ℕ) : ↑n.succ = Order.succ ↑n

@[implicit_reducible]

instance Ordinal.uniqueIioOne : Unique ↑(Set.Iio 1)

@[simp]

theorem Ordinal.Iio_one_default_eq : default = ⟨0, ⋯⟩

@[implicit_reducible]

noncomputable instance Ordinal.uniqueToTypeOne : Unique (ToType 1)

theorem Ordinal.one_toType_eq (x : ToType 1) : x = (enum fun (x1 x2 : ToType 1) => x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

theorem Ordinal.type_lt_mem_range_succ_iff {α : Type u} [LinearOrder α] [WellFoundedLT α] : (type fun (x1 x2 : α) => x1 < x2) ∈ Set.range Order.succ ↔ ∃ (x : α), IsMax x

theorem Ordinal.type_lt_mem_range_succ {α : Type u} [LinearOrder α] [WellFoundedLT α] [OrderTop α] : (type fun (x1 x2 : α) => x1 < x2) ∈ Set.range Order.succ

theorem Ordinal.isSuccPrelimit_type_lt_iff {α : Type u} [LinearOrder α] [WellFoundedLT α] : Order.IsSuccPrelimit (type fun (x1 x2 : α) => x1 < x2) ↔ NoMaxOrder α

theorem Ordinal.isSuccPrelimit_type_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] [h : NoMaxOrder α] : Order.IsSuccPrelimit (type fun (x1 x2 : α) => x1 < x2)

Extra properties of typein and enum

@[simp]

theorem Ordinal.typein_one_toType (x : ToType 1) : (typein fun (x1 x2 : ToType 1) => x1 < x2).toRelEmbedding x = 0

theorem Ordinal.typein_le_typein' (o : Ordinal.{u_1}) {x y : o.ToType} : (typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding x ≤ (typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding y ↔ x ≤ y

theorem Ordinal.le_enum_succ {o : Ordinal.{u_1}} (a : (Order.succ o).ToType) : a ≤ (enum fun (x1 x2 : (Order.succ o).ToType) => x1 < x2) ⟨o, ⋯⟩

Universal ordinal

def Ordinal.univ : Ordinal.{max (u + 1) v}

univ.{u v} is the order type of the ordinals of Type u as a member of Ordinal.{v} (when u < v). It is an inaccessible cardinal.

@[simp]

theorem Ordinal.type_lt_ordinal : (type fun (x1 x2 : Ordinal.{u}) => x1 < x2) = univ.{u, u + 1}

@[deprecated Ordinal.type_lt_ordinal (since := "2026-03-20")]

theorem Ordinal.univ_id : univ.{u, u + 1} = type fun (x1 x2 : Ordinal.{u}) => x1 < x2

@[simp]

theorem Ordinal.lift_univ : lift.{w, max (u + 1) v} univ.{u, v} = univ.{u, max v w}

theorem Ordinal.univ_umax : univ.{u, max (u + 1) v} = univ.{u, v}

def Ordinal.liftPrincipalSeg : PrincipalSeg (fun (x1 x2 : Ordinal.{u}) => x1 < x2) fun (x1 x2 : Ordinal.{max (u + 1) v}) => x1 < x2

Principal segment version of the lift operation on ordinals, embedding Ordinal.{u} in Ordinal.{v} as a principal segment when u < v.

@[simp]

theorem Ordinal.liftPrincipalSeg_coe : ⇑liftPrincipalSeg.toRelEmbedding = lift.{max (u + 1) v, u}

@[simp]

theorem Ordinal.liftPrincipalSeg_top : liftPrincipalSeg.top = univ.{u, v}

@[deprecated Ordinal.liftPrincipalSeg_top (since := "2026-03-20")]

theorem Ordinal.liftPrincipalSeg_top' : liftPrincipalSeg.top = type fun (x1 x2 : Ordinal.{u}) => x1 < x2

Representing a cardinal with an ordinal

@[simp]

theorem Cardinal.mk_toType (o : Ordinal.{u_1}) : mk o.ToType = o.card

noncomputable def Cardinal.ord (c : Cardinal.{u}) : Ordinal.{u}

The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c. For the order-embedding version, see ord.order_embedding.

theorem Cardinal.ord_eq_iInf (α : Type u) : (mk α).ord = ⨅ (r : { r : α → α → Prop // IsWellOrder α r }), Ordinal.type ↑r

@[deprecated Cardinal.ord_eq_iInf (since := "2026-03-15")]

theorem Cardinal.ord_eq_Inf (α : Type u) : (mk α).ord = ⨅ (r : { r : α → α → Prop // IsWellOrder α r }), Ordinal.type ↑r

Alias of Cardinal.ord_eq_iInf.

theorem Cardinal.exists_ord_eq (α : Type u_1) : ∃ (r : α → α → Prop) (x : IsWellOrder α r), (mk α).ord = Ordinal.type r

There exists a well-order on α whose order type is exactly ord #α.

@[deprecated Cardinal.exists_ord_eq (since := "2026-03-29")]

theorem Cardinal.ord_eq (α : Type u_1) : ∃ (r : α → α → Prop) (x : IsWellOrder α r), (mk α).ord = Ordinal.type r

Alias of Cardinal.exists_ord_eq.

---

There exists a well-order on α whose order type is exactly ord #α.

theorem Cardinal.exists_ord_eq_type_lt (α : Type u_1) : ∃ (x : LinearOrder α) (x_1 : WellFoundedLT α), (mk α).ord = Ordinal.type fun (x1 x2 : α) => x1 < x2

There exists a well-order on α whose order type is exactly ord #α.

theorem Cardinal.ord_le_type {α : Type u} (r : α → α → Prop) [h : IsWellOrder α r] : (mk α).ord ≤ Ordinal.type r

theorem Cardinal.ord_le {c : Cardinal.{u_1}} {o : Ordinal.{u_1}} : c.ord ≤ o ↔ c ≤ o.card

theorem Cardinal.gc_ord_card : GaloisConnection ord Ordinal.card

theorem Cardinal.lt_ord {c : Cardinal.{u_1}} {o : Ordinal.{u_1}} : o < c.ord ↔ o.card < c

@[simp]

theorem Cardinal.card_ord (c : Cardinal.{u_1}) : c.ord.card = c

theorem Cardinal.card_surjective : Function.Surjective Ordinal.card

theorem Cardinal.bddAbove_ord_image_iff {s : Set Cardinal.{u_1}} : BddAbove (ord '' s) ↔ BddAbove s

noncomputable def Cardinal.gciOrdCard : GaloisCoinsertion ord Ordinal.card

Galois coinsertion between Cardinal.ord and Ordinal.card.

theorem Cardinal.ord_card_le (o : Ordinal.{u_1}) : o.card.ord ≤ o

theorem Cardinal.lt_ord_succ_card (o : Ordinal.{u_1}) : o < (Order.succ o.card).ord

theorem Cardinal.card_le_iff {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} : o.card ≤ c ↔ o < (Order.succ c).ord

theorem Cardinal.card_le_of_le_ord {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} (ho : o ≤ c.ord) : o.card ≤ c

A variation on Cardinal.lt_ord using ≤: If o is no greater than the initial ordinal of cardinality c, then its cardinal is no greater than c.

The converse, however, is false (for instance, o = ω+1 and c = ℵ₀).

theorem Cardinal.ord_strictMono : StrictMono ord

theorem Cardinal.ord_mono : Monotone ord

@[simp]

theorem Cardinal.ord_le_ord {c₁ c₂ : Cardinal.{u_1}} : c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂

@[simp]

theorem Cardinal.ord_lt_ord {c₁ c₂ : Cardinal.{u_1}} : c₁.ord < c₂.ord ↔ c₁ < c₂

@[simp]

theorem Cardinal.ord_zero : ord 0 = 0

@[simp]

theorem Cardinal.ord_nat (n : ℕ) : (↑n).ord = ↑n

@[simp]

theorem Cardinal.ord_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).ord = OfNat.ofNat n

@[simp]

theorem Cardinal.ord_one : ord 1 = 1

theorem Cardinal.isNormal_ord : Order.IsNormal ord

@[simp]

theorem Cardinal.ord_aleph0 : aleph0.ord = Ordinal.omega0

@[simp]

theorem Cardinal.lift_ord (c : Cardinal.{v}) : Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

theorem Cardinal.mk_ord_toType (c : Cardinal.{u_1}) : mk c.ord.ToType = c

theorem Cardinal.card_typein_lt {α : Type u} {r : α → α → Prop} [IsWellOrder α r] (x : α) (h : (mk α).ord = Ordinal.type r) : ((Ordinal.typein r).toRelEmbedding x).card < mk α

theorem Cardinal.mk_Iio_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] (i : α) (h : (mk α).ord = Ordinal.type fun (x1 x2 : α) => x1 < x2) : mk ↑(Set.Iio i) < mk α

theorem Cardinal.mk_Iio_toType_ord_lt {c : Cardinal.{u_1}} (i : c.ord.ToType) : mk ↑(Set.Iio i) < c

@[deprecated Cardinal.mk_Iio_toType_ord_lt (since := "2026-03-20")]

theorem Cardinal.mk_Iio_ord_toType {c : Cardinal.{u_1}} (i : c.ord.ToType) : mk ↑(Set.Iio i) < c

Alias of Cardinal.mk_Iio_toType_ord_lt.

@[deprecated Cardinal.mk_Iio_toType_ord_lt (since := "2026-03-20")]

theorem Cardinal.card_typein_toType_lt (c : Cardinal.{u_1}) (x : c.ord.ToType) : ((Ordinal.typein fun (x1 x2 : c.ord.ToType) => x1 < x2).toRelEmbedding x).card < c

theorem Cardinal.ord_injective : Function.Injective ord

@[simp]

theorem Cardinal.ord_inj {a b : Cardinal.{u_1}} : a.ord = b.ord ↔ a = b

@[simp]

theorem Cardinal.ord_eq_zero {a : Cardinal.{u_1}} : a.ord = 0 ↔ a = 0

@[simp]

theorem Cardinal.ord_eq_one {a : Cardinal.{u_1}} : a.ord = 1 ↔ a = 1

@[simp]

theorem Cardinal.ord_pos {a : Cardinal.{u_1}} : 0 < a.ord ↔ 0 < a

@[simp]

theorem Cardinal.omega0_le_ord {a : Cardinal.{u_1}} : Ordinal.omega0 ≤ a.ord ↔ aleph0 ≤ a

@[simp]

theorem Cardinal.ord_le_omega0 {a : Cardinal.{u_1}} : a.ord ≤ Ordinal.omega0 ↔ a ≤ aleph0

@[simp]

theorem Cardinal.ord_lt_omega0 {a : Cardinal.{u_1}} : a.ord < Ordinal.omega0 ↔ a < aleph0

@[simp]

theorem Cardinal.omega0_lt_ord {a : Cardinal.{u_1}} : Ordinal.omega0 < a.ord ↔ aleph0 < a

@[simp]

theorem Cardinal.ord_eq_omega0 {a : Cardinal.{u_1}} : a.ord = Ordinal.omega0 ↔ a = aleph0

noncomputable def Cardinal.ord.orderEmbedding : Cardinal.{u_1} ↪o Ordinal.{u_1}

The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c. This is the order-embedding version. For the regular function, see ord.

@[simp]

theorem Cardinal.ord.orderEmbedding_coe : ⇑orderEmbedding = ord

def Cardinal.univ : Cardinal.{max (u + 1) v}

The cardinal univ is the cardinality of ordinal univ, or equivalently the cardinal of Ordinal.{u}, or Cardinal.{u}, as an element of Cardinal.{v} (when u < v).

theorem Cardinal.univ_id : univ.{u, u + 1} = mk Ordinal.{u}

@[simp]

theorem Cardinal.lift_univ : lift.{w, max (u + 1) v} univ.{u, v} = univ.{u, max v w}

theorem Cardinal.univ_umax : univ.{u, max (u + 1) v} = univ.{u, v}

theorem Cardinal.lift_lt_univ (c : Cardinal.{u}) : lift.{u + 1, u} c < univ.{u, u + 1}

theorem Cardinal.lift_lt_univ' (c : Cardinal.{u}) : lift.{max (u + 1) v, u} c < univ.{u, v}

theorem Cardinal.aleph0_lt_univ : aleph0 < univ.{u, v}

theorem Cardinal.nat_lt_univ (n : ℕ) : ↑n < univ.{u, v}

theorem Cardinal.univ_pos : 0 < univ.{u, v}

theorem Cardinal.univ_ne_zero : univ.{u, v} ≠ 0

@[simp]

theorem Cardinal.ord_univ : univ.{u, v}.ord = Ordinal.univ.{u, v}

theorem Cardinal.lt_univ {c : Cardinal.{u + 1}} : c < univ.{u, u + 1} ↔ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'

theorem Cardinal.lt_univ' {c : Cardinal.{max (u + 1) v}} : c < univ.{u, v} ↔ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'

theorem Cardinal.IsStrongLimit.univ : Cardinal.univ.{u, v}.IsStrongLimit

theorem Cardinal.small_iff_lift_mk_lt_univ {α : Type u} : Small.{v, u} α ↔ lift.{v + 1, u} (mk α) < univ.{v, max u (v + 1)}

@[implicit_reducible]

noncomputable def Cardinal.toTypeOrderBot {c : Cardinal.{u_1}} (hc : c ≠ 0) : OrderBot c.ord.ToType

If a cardinal c is nonzero, then c.ord.ToType has a least element.

@[simp]

theorem Ordinal.card_univ : univ.{u, v}.card = Cardinal.univ.{u, v}

@[simp]

theorem Ordinal.nat_le_card {o : Ordinal.{u_1}} {n : ℕ} : ↑n ≤ o.card ↔ ↑n ≤ o

@[simp]

theorem Ordinal.one_le_card {o : Ordinal.{u_1}} : 1 ≤ o.card ↔ 1 ≤ o

@[simp]

theorem Ordinal.ofNat_le_card {o : Ordinal.{u_1}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n ≤ o.card ↔ OfNat.ofNat n ≤ o

@[simp]

theorem Ordinal.aleph0_le_card {o : Ordinal.{u_1}} : Cardinal.aleph0 ≤ o.card ↔ omega0 ≤ o

@[simp]

theorem Ordinal.card_lt_aleph0 {o : Ordinal.{u_1}} : o.card < Cardinal.aleph0 ↔ o < omega0

@[simp]

theorem Ordinal.nat_lt_card {o : Ordinal.{u_1}} {n : ℕ} : ↑n < o.card ↔ ↑n < o

@[simp]

theorem Ordinal.zero_lt_card {o : Ordinal.{u_1}} : 0 < o.card ↔ 0 < o

@[simp]

theorem Ordinal.one_lt_card {o : Ordinal.{u_1}} : 1 < o.card ↔ 1 < o

@[simp]

theorem Ordinal.ofNat_lt_card {o : Ordinal.{u_1}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n < o.card ↔ OfNat.ofNat n < o

@[simp]

theorem Ordinal.card_lt_nat {o : Ordinal.{u_1}} {n : ℕ} : o.card < ↑n ↔ o < ↑n

@[simp]

theorem Ordinal.card_lt_ofNat {o : Ordinal.{u_1}} {n : ℕ} [n.AtLeastTwo] : o.card < OfNat.ofNat n ↔ o < OfNat.ofNat n

@[simp]

theorem Ordinal.card_le_nat {o : Ordinal.{u_1}} {n : ℕ} : o.card ≤ ↑n ↔ o ≤ ↑n

@[simp]

theorem Ordinal.card_le_one {o : Ordinal.{u_1}} : o.card ≤ 1 ↔ o ≤ 1

@[simp]

theorem Ordinal.card_le_ofNat {o : Ordinal.{u_1}} {n : ℕ} [n.AtLeastTwo] : o.card ≤ OfNat.ofNat n ↔ o ≤ OfNat.ofNat n

@[simp]

theorem Ordinal.card_eq_nat {o : Ordinal.{u_1}} {n : ℕ} : o.card = ↑n ↔ o = ↑n

@[simp]

theorem Ordinal.card_eq_zero {o : Ordinal.{u_1}} : o.card = 0 ↔ o = 0

@[simp]

theorem Ordinal.card_eq_one {o : Ordinal.{u_1}} : o.card = 1 ↔ o = 1

theorem Cardinal.le_ord_iff_card_le_of_lt_aleph0 (o : Ordinal.{u_1}) {c : Cardinal.{u_1}} (hc : c < aleph0) : o ≤ c.ord ↔ o.card ≤ c

theorem Ordinal.mem_range_lift_of_card_le {a : Cardinal.{u}} {b : Ordinal.{max u v}} (h : b.card ≤ Cardinal.lift.{v, u} a) : b ∈ Set.range lift.{v, u}

@[simp]

theorem Ordinal.card_eq_ofNat {o : Ordinal.{u_1}} {n : ℕ} [n.AtLeastTwo] : o.card = OfNat.ofNat n ↔ o = OfNat.ofNat n

@[simp]

theorem Ordinal.type_fintype {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [Fintype α] : type r = ↑(Fintype.card α)

theorem Ordinal.type_fin (n : ℕ) : (type fun (x1 x2 : Fin n) => x1 < x2) = ↑n

theorem Ordinal.ord_mk_le_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (s : Set α) : (Cardinal.mk ↑s).ord ≤ type r

theorem Ordinal.ord_mk_lt_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty) : (Cardinal.mk ↑s).ord < type r

theorem Ordinal.not_lt_enum_ord_mk_min_compl {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty) : ¬r ((enum r) ⟨(Cardinal.mk ↑s).ord, ⋯⟩) (⋯.min sᶜ h)

The #s-th element of α is an upper-bound for the set's mex (minimum excluded value), ordered by r, when s is finite. See card_typein_min_le_mk for the Ordinal version.

Sorted lists

theorem List.SortedGT.lt_ord_of_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] {l m : List α} {o : Ordinal.{u}} (hl : l.SortedGT) (hm : m.SortedGT) (hmltl : m < l) (hlt : ∀ i ∈ l, (Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding i < o) (i : α) : i ∈ m → (Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding i < o

@[deprecated List.SortedGT.lt_ord_of_lt (since := "2025-11-27")]

theorem List.Sorted.lt_ord_of_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] {l m : List α} {o : Ordinal.{u}} (hl : l.SortedGT) (hm : m.SortedGT) (hmltl : m < l) (hlt : ∀ i ∈ l, (Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding i < o) (i : α) : i ∈ m → (Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding i < o

Alias of List.SortedGT.lt_ord_of_lt.