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.

Notations

• ω is a notation for the first infinite ordinal in the locale 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 α.

instance WellOrder.inhabited : Inhabited WellOrder

Equations

• WellOrder.inhabited = { default := { α := PEmpty.{?u.3 + 1}, r := EmptyRelation, wo := WellOrder.inhabited.proof_1 } }

@[deprecated "No deprecation message was provided." (since := "2024-10-24")]

theorem WellOrder.eta (o : WellOrder) : { α := o.α, r := o.r, wo := ⋯ } = o

instance Ordinal.isEquivalent : Setoid WellOrder

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

Equations

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

def Ordinal : Type (u + 1)

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

Equations

• Ordinal.{?u.3} = Quotient Ordinal.isEquivalent

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.

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

Equations

• o.toType = (Quotient.out o).α

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

Equations

• hasWellFounded_toType o = { rel := (Quotient.out o).r, wf := ⋯ }

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

Equations

• linearOrder_toType o = IsWellOrder.linearOrder (Quotient.out o).r

instance wellFoundedLT_toType_lt (o : Ordinal.{u_1}) : WellFoundedLT 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.

Equations

• Ordinal.type r = ⟦{ α := α, r := r, wo := wo }⟧

def Ordinal.termTypeLT_ : Lean.ParserDescr

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

Equations

• Ordinal.termTypeLT_ = Lean.ParserDescr.node `Ordinal.termTypeLT_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "typeLT ") (Lean.ParserDescr.cat `term 70))

instance Ordinal.zero : Zero Ordinal.{u_1}

Equations

• Ordinal.zero = { zero := Ordinal.type EmptyRelation }

instance Ordinal.inhabited : Inhabited Ordinal.{u_1}

Equations

• Ordinal.inhabited = { default := 0 }

instance Ordinal.one : One Ordinal.{u_1}

Equations

• Ordinal.one = { one := Ordinal.type EmptyRelation }

@[deprecated "Avoid using `Quotient.mk` to construct an `Ordinal` directly." (since := "2024-10-24")]

theorem Ordinal.type_def' (w : WellOrder) : ⟦w⟧ = Ordinal.type w.r

@[deprecated "Avoid using `Quotient.mk` to construct an `Ordinal` directly." (since := "2024-10-24")]

theorem Ordinal.type_def {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] : ⟦{ α := α, r := r, wo := wo }⟧ = Ordinal.type r

@[simp]

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

@[deprecated Ordinal.type_toType (since := "2024-10-22")]

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

@[deprecated Ordinal.type_toType (since := "2024-08-26")]

theorem Ordinal.type_out (o : Ordinal.{u_1}) : Ordinal.type (Quotient.out o).r = o

theorem Ordinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type r = Ordinal.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 α] : Ordinal.type r = 0

@[simp]

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

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

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

theorem Ordinal.type_pEmpty : Ordinal.type EmptyRelation = 0

theorem Ordinal.type_empty : Ordinal.type EmptyRelation = 0

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

@[simp]

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

theorem Ordinal.type_pUnit : Ordinal.type EmptyRelation = 1

theorem Ordinal.type_unit : Ordinal.type EmptyRelation = 1

@[simp]

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

@[deprecated Ordinal.toType_empty_iff_eq_zero (since := "2024-08-26")]

theorem Ordinal.out_empty_iff_eq_zero {o : Ordinal.{u_1}} : IsEmpty o.toType ↔ o = 0

Alias of Ordinal.toType_empty_iff_eq_zero.

@[deprecated Ordinal.toType_empty_iff_eq_zero (since := "2024-08-26")]

theorem Ordinal.eq_zero_of_out_empty (o : Ordinal.{u_1}) [h : IsEmpty o.toType] : o = 0

instance Ordinal.isEmpty_toType_zero : IsEmpty (Ordinal.toType 0)

@[simp]

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

@[deprecated Ordinal.toType_nonempty_iff_ne_zero (since := "2024-08-26")]

theorem Ordinal.out_nonempty_iff_ne_zero {o : Ordinal.{u_1}} : Nonempty o.toType ↔ o ≠ 0

Alias of Ordinal.toType_nonempty_iff_ne_zero.

@[deprecated Ordinal.toType_nonempty_iff_ne_zero (since := "2024-08-26")]

theorem Ordinal.ne_zero_of_out_nonempty (o : Ordinal.{u_1}) [h : Nonempty o.toType] : o ≠ 0

theorem Ordinal.one_ne_zero : 1 ≠ 0

instance Ordinal.nontrivial : Nontrivial Ordinal.{u}

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

Quotient.inductionOn specialized to ordinals.

Not to be confused with well-founded recursion Ordinal.induction.

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

Quotient.inductionOn₂ specialized to ordinals.

Not to be confused with well-founded recursion Ordinal.induction.

theorem Ordinal.inductionOn₃ {C : Ordinal.{u_1} → Ordinal.{u_2} → Ordinal.{u_3} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}) (o₃ : Ordinal.{u_3}) (H : ∀ (α : 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], C (Ordinal.type r) (Ordinal.type s) (Ordinal.type t)) : C o₁ o₂ o₃

Quotient.inductionOn₃ specialized to ordinals.

Not to be confused with well-founded recursion Ordinal.induction.

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

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

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

Equations

• o.liftOnWellOrder f c = Quotient.liftOn o (fun (w : WellOrder) => f w.α) ⋯

@[simp]

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

The order on ordinals

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 Order.InitialSeg file.

Equations

• Ordinal.partialOrder = PartialOrder.mk Ordinal.partialOrder.proof_6

instance Ordinal.instLinearOrder : LinearOrder Ordinal.{u_1}

Equations

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

theorem InitialSeg.ordinal_type_le {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≼i 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 : r ≺i s) : Ordinal.type r < Ordinal.type s

@[simp]

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

instance Ordinal.instOrderBot : OrderBot Ordinal.{u_1}

Equations

• Ordinal.instOrderBot = OrderBot.mk Ordinal.zero_le

@[simp]

theorem Ordinal.bot_eq_zero : ⊥ = 0

@[simp]

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

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

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

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] : Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ≼i s)

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

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

def Ordinal.initialSegToType {α β : Ordinal.{u_1}} (h : α ≤ β) : (fun (x1 x2 : α.toType) => x1 < x2) ≼i fun (x1 x2 : β.toType) => x1 < x2

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

Equations

• Ordinal.initialSegToType h = Classical.choice ⋯

@[deprecated Ordinal.initialSegToType (since := "2024-08-26")]

def Ordinal.initialSegOut {α β : Ordinal.{u_1}} (h : α ≤ β) : (fun (x1 x2 : α.toType) => x1 < x2) ≼i fun (x1 x2 : β.toType) => x1 < x2

Alias of Ordinal.initialSegToType.

---

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

Equations

• @Ordinal.initialSegOut = @Ordinal.initialSegToType

def Ordinal.principalSegToType {α β : Ordinal.{u_1}} (h : α < β) : (fun (x1 x2 : α.toType) => x1 < x2) ≺i fun (x1 x2 : β.toType) => x1 < x2

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

Equations

• Ordinal.principalSegToType h = Classical.choice ⋯

@[deprecated Ordinal.principalSegToType (since := "2024-08-26")]

def Ordinal.principalSegOut {α β : Ordinal.{u_1}} (h : α < β) : (fun (x1 x2 : α.toType) => x1 < x2) ≺i fun (x1 x2 : β.toType) => x1 < x2

Alias of Ordinal.principalSegToType.

---

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

Equations

• @Ordinal.principalSegOut = @Ordinal.principalSegToType

Enumerating elements in a well-order with ordinals

def Ordinal.typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : r ≺i 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.

Equations

• Ordinal.typein r = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => Ordinal.type (Subrel r {b : α | r b a})) ⋯, top := Ordinal.type r, mem_range_iff_rel' := ⋯ }

@[deprecated Ordinal.typein (since := "2024-10-09")]

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

Alias of Ordinal.typein.

---

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.

Equations

• @Ordinal.typein.principalSeg = @Ordinal.typein

@[deprecated "No deprecation message was provided." (since := "2024-10-09")]

theorem Ordinal.typein.principalSeg_coe {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : ⇑(Ordinal.typein.principalSeg r).toRelEmbedding = ⇑(Ordinal.typein r).toRelEmbedding

@[simp]

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

@[simp]

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

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

theorem Ordinal.typein_lt_self {o : Ordinal.{u_1}} (i : o.toType) : (Ordinal.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 : r ≺i s) : (Ordinal.typein s).toRelEmbedding f.top = Ordinal.type r

@[simp]

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

@[simp]

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

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

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

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

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

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

def Ordinal.enum {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : Subrel (fun (x1 x2 : Ordinal.{u}) => x1 < x2) {o : Ordinal.{u} | o < Ordinal.type r} ≃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 α.

Equations

• Ordinal.enum r = (Ordinal.typein r).subrelIso

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

theorem Ordinal.enum_zero_le' {o : Ordinal.{u_1}} (h0 : 0 < o) (a : o.toType) : (Ordinal.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 < Ordinal.type r) (hs : o < Ordinal.type s) : f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.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 < Ordinal.type r) : f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.enum s) ⟨o, ⋯⟩

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

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

Equations

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

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

theorem Ordinal.enumIsoToType_symm_apply_coe (o : Ordinal.{u_1}) (x : o.toType) : ↑((RelIso.symm o.enumIsoToType) x) = (Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding x

@[deprecated Ordinal.enumIsoToType "No deprecation message was provided." (since := "2024-08-26")]

def Ordinal.enumIsoOut (o : Ordinal.{u_1}) : ↑(Set.Iio o) ≃o o.toType

Alias of Ordinal.enumIsoToType.

---

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

Equations

• Ordinal.enumIsoOut = Ordinal.enumIsoToType

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)

def Ordinal.toTypeOrderBotOfPos {o : Ordinal.{u_1}} (ho : 0 < o) : OrderBot o.toType

o.toType is an OrderBot whenever 0 < o.

Equations

• Ordinal.toTypeOrderBotOfPos ho = OrderBot.mk ⋯

@[deprecated Ordinal.toTypeOrderBotOfPos (since := "2024-08-26")]

def Ordinal.outOrderBotOfPos {o : Ordinal.{u_1}} (ho : 0 < o) : OrderBot o.toType

Alias of Ordinal.toTypeOrderBotOfPos.

---

o.toType is an OrderBot whenever 0 < o.

Equations

• @Ordinal.outOrderBotOfPos = @Ordinal.toTypeOrderBotOfPos

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

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

instance Ordinal.wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}

Equations

• Ordinal.wellFoundedRelation = { rel := fun (x1 x2 : Ordinal.{?u.5}) => x1 < x2, wf := Ordinal.lt_wf }

instance Ordinal.wellFoundedLT : WellFoundedLT Ordinal.{u_1}

instance Ordinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Ordinal.{u_1}

Equations

• Ordinal.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot Ordinal.{?u.3}

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

Reformulation of well founded induction on ordinals as a lemma that works with the induction tactic, as in induction i using Ordinal.induction with | h i IH => ?_.

theorem Ordinal.typein_apply {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (a : α) : (Ordinal.typein s).toRelEmbedding (f a) = (Ordinal.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.

Equations

• Ordinal.card = Quotient.map WellOrder.α Ordinal.card.proof_1

@[simp]

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

@[simp]

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

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

@[simp]

theorem Ordinal.card_zero : Ordinal.card 0 = 0

@[simp]

theorem Ordinal.card_one : Ordinal.card 1 = 1

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.

Equations

• Ordinal.lift.{?u.12, ?u.11} o = Quotient.liftOn o (fun (w : WellOrder) => Ordinal.type (ULift.down ⁻¹'o w.r)) Ordinal.lift.proof_2

@[simp]

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

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 : β ≃ α) : Ordinal.type (⇑f ⁻¹'o r) = Ordinal.type r

@[simp]

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

@[deprecated Ordinal.type_lift_preimage_aux (since := "2024-10-22")]

theorem Ordinal.type_lift_preimage_aux {α : Type u} {β : Type v} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : Ordinal.lift.{u, v} (Ordinal.type fun (x y : β) => r (f x) (f y)) = Ordinal.lift.{v, u} (Ordinal.type r)

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

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

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

@[deprecated Ordinal.lift_umax (since := "2024-10-24")]

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

lift.{max v u, 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}) : Ordinal.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}) : Ordinal.lift.{u, u} a = a

An ordinal lifted to the same universe equals itself.

@[simp]

theorem Ordinal.lift_uzero (a : Ordinal.{u}) : Ordinal.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] : Ordinal.lift.{max v w, u} (Ordinal.type r) ≤ Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≼i s)

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Ordinal.lift_lt {a b : Ordinal.{v}} : Ordinal.lift.{u, v} a < Ordinal.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 : r ≺i s) : Ordinal.lift.{u, v} ((Ordinal.typein s).toRelEmbedding f.top) = Ordinal.lift.{v, u} (Ordinal.type r)

def Ordinal.liftInitialSeg : (fun (x1 x2 : Ordinal.{v}) => x1 < x2) ≼i 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.

Equations

• Ordinal.liftInitialSeg = { toRelEmbedding := RelEmbedding.ofMonotone Ordinal.lift.{?u.22, ?u.21} Ordinal.liftInitialSeg.proof_2, mem_range_of_rel' := Ordinal.liftInitialSeg.proof_3 }

@[deprecated Ordinal.liftInitialSeg (since := "2024-09-21")]

def Ordinal.lift.initialSeg : (fun (x1 x2 : Ordinal.{v}) => x1 < x2) ≼i fun (x1 x2 : Ordinal.{max u v}) => x1 < x2

Alias of Ordinal.liftInitialSeg.

---

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

Equations

• Ordinal.lift.initialSeg = Ordinal.liftInitialSeg

@[simp]

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

@[deprecated Ordinal.liftInitialSeg_coe (since := "2024-09-21")]

theorem Ordinal.lift.initialSeg_coe : ⇑Ordinal.lift.initialSeg = Ordinal.lift.{v, u}

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[deprecated Ordinal.mem_range_lift_of_le (since := "2024-10-07")]

theorem Ordinal.lift_down {a : Ordinal.{u}} {b : Ordinal.{max u v}} (h : b ≤ Ordinal.lift.{v, u} a) : ∃ (a' : Ordinal.{u}), Ordinal.lift.{v, u} a' = b

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

theorem Ordinal.lt_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v}} : b < Ordinal.lift.{v, u} a ↔ ∃ a' < a, Ordinal.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 ℕ.

Equations

• Ordinal.omega0 = Ordinal.lift.{?u.5, 0} (Ordinal.type fun (x1 x2 : ℕ) => x1 < x2)

def Ordinal.termω : Lean.ParserDescr

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

Equations

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Ordinal.lift_omega0 : Ordinal.lift.{u_1, u_2} Ordinal.omega0 = Ordinal.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.

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₂.

Equations

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

instance Ordinal.addMonoidWithOne : AddMonoidWithOne Ordinal.{u}

Equations

• Ordinal.addMonoidWithOne = AddMonoidWithOne.mk Ordinal.addMonoidWithOne.proof_6 Ordinal.addMonoidWithOne.proof_7

@[simp]

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

@[simp]

theorem Ordinal.type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type (Sum.Lex r s) = Ordinal.type r + Ordinal.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}

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

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

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

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

@[simp]

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

@[simp]

theorem Ordinal.sInf_empty : sInf ∅ = 0

Successor order properties

instance Ordinal.instNoMaxOrder : NoMaxOrder Ordinal.{u_1}

instance Ordinal.instSuccOrder : SuccOrder Ordinal.{u}

Equations

• Ordinal.instSuccOrder = SuccOrder.ofSuccLeIff (fun (o : Ordinal.{?u.6}) => o + 1) ⋯

instance Ordinal.instSuccAddOrder : SuccAddOrder Ordinal.{u_1}

Equations

• Ordinal.instSuccAddOrder = SuccAddOrder.mk Ordinal.instSuccAddOrder.proof_1

@[simp]

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

@[simp]

theorem Ordinal.succ_zero : Order.succ 0 = 1

@[simp]

theorem Ordinal.succ_one : Order.succ 1 = 2

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

@[deprecated Order.one_le_iff_pos (since := "2024-09-04")]

theorem Ordinal.one_le_iff_pos {o : Ordinal.{u_1}} : 1 ≤ o ↔ 0 < o

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.succ_ne_zero (o : Ordinal.{u_1}) : Order.succ o ≠ 0

@[simp]

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

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

@[simp]

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

@[deprecated Ordinal.natCast_succ "No deprecation message was provided." (since := "2024-04-17")]

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

Alias of Ordinal.natCast_succ.

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

Equations

• Ordinal.uniqueIioOne = { default := ⟨0, Ordinal.uniqueIioOne.proof_1⟩, uniq := Ordinal.uniqueIioOne.proof_2 }

instance Ordinal.uniqueToTypeOne : Unique (Ordinal.toType 1)

Equations

• Ordinal.uniqueToTypeOne = { default := (Ordinal.enum fun (x1 x2 : Ordinal.toType 1) => x1 < x2) ⟨0, Ordinal.uniqueToTypeOne.proof_2⟩, uniq := Ordinal.uniqueToTypeOne.proof_3 }

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

@[deprecated Ordinal.one_toType_eq (since := "2024-08-26")]

theorem Ordinal.one_out_eq (x : Ordinal.toType 1) : x = (Ordinal.enum fun (x1 x2 : Ordinal.toType 1) => x1 < x2) ⟨0, ⋯⟩

Alias of Ordinal.one_toType_eq.

Extra properties of typein and enum

@[simp]

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

@[deprecated Ordinal.typein_one_toType (since := "2024-08-26")]

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

Alias of Ordinal.typein_one_toType.

theorem Ordinal.typein_le_typein' (o : Ordinal.{u_1}) {x y : o.toType} : (Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding x ≤ (Ordinal.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 ≤ (Ordinal.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.

Equations

• Ordinal.univ.{?u.2, ?u.1} = Ordinal.lift.{?u.1, ?u.2 + 1} (Ordinal.type fun (x1 x2 : Ordinal.{?u.2}) => x1 < x2)

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

@[simp]

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

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

def Ordinal.liftPrincipalSeg : (fun (x1 x2 : Ordinal.{u}) => x1 < x2) ≺i 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.

Equations

• Ordinal.liftPrincipalSeg = { toRelEmbedding := Ordinal.liftInitialSeg.toRelEmbedding, top := Ordinal.univ.{?u.26, ?u.25}, mem_range_iff_rel' := Ordinal.liftPrincipalSeg.proof_1 }

@[deprecated Ordinal.liftPrincipalSeg (since := "2024-09-21")]

def Ordinal.lift.principalSeg : (fun (x1 x2 : Ordinal.{u}) => x1 < x2) ≺i fun (x1 x2 : Ordinal.{max (u + 1) v}) => x1 < x2

Alias of Ordinal.liftPrincipalSeg.

---

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

Equations

• Ordinal.lift.principalSeg = Ordinal.liftPrincipalSeg

@[simp]

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

@[deprecated Ordinal.liftPrincipalSeg_coe (since := "2024-09-21")]

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

@[simp]

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

@[deprecated Ordinal.liftPrincipalSeg_top (since := "2024-09-21")]

theorem Ordinal.lift.principalSeg_top : Ordinal.lift.principalSeg.top = Ordinal.univ.{u, v}

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

@[deprecated Ordinal.liftPrincipalSeg_top (since := "2024-09-21")]

theorem Ordinal.lift.principalSeg_top' : Ordinal.lift.principalSeg.top = Ordinal.type fun (x1 x2 : Ordinal.{u}) => x1 < x2

Representing a cardinal with an ordinal

@[simp]

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

@[deprecated Cardinal.mk_toType (since := "2024-08-26")]

theorem Cardinal.mk_ordinal_out (o : Ordinal.{u_1}) : Cardinal.mk o.toType = o.card

Alias of Cardinal.mk_toType.

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.

Equations

• c.ord = Quot.liftOn c (fun (α : Type ?u.18) => ⨅ (r : { r : α → α → Prop // IsWellOrder α r }), Ordinal.type ↑r) Cardinal.ord.proof_2

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

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

theorem Cardinal.ord_le_type {α : Type u} (r : α → α → Prop) [h : IsWellOrder α r] : (Cardinal.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 Cardinal.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

def Cardinal.gciOrdCard : GaloisCoinsertion Cardinal.ord Ordinal.card

Galois coinsertion between Cardinal.ord and Ordinal.card.

Equations

• Cardinal.gciOrdCard = Cardinal.gc_ord_card.toGaloisCoinsertion Cardinal.gciOrdCard.proof_1

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 Cardinal.ord

theorem Cardinal.ord_mono : Monotone Cardinal.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 : Cardinal.ord 0 = 0

@[simp]

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

@[simp]

theorem Cardinal.ord_one : Cardinal.ord 1 = 1

@[simp]

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

@[simp]

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

@[simp]

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

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

@[deprecated Cardinal.mk_ord_toType (since := "2024-08-26")]

theorem Cardinal.mk_ord_out (c : Cardinal.{u_1}) : Cardinal.mk c.ord.toType = c

Alias of Cardinal.mk_ord_toType.

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

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

@[deprecated Cardinal.card_typein_toType_lt (since := "2024-08-26")]

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

Alias of Cardinal.card_typein_toType_lt.

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

@[deprecated Cardinal.mk_Iio_ord_toType "No deprecation message was provided." (since := "2024-08-26")]

theorem Cardinal.mk_Iio_ord_out_α {c : Cardinal.{u_1}} (i : c.ord.toType) : Cardinal.mk ↑(Set.Iio i) < c

Alias of Cardinal.mk_Iio_ord_toType.

theorem Cardinal.ord_injective : Function.Injective Cardinal.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.omega0_le_ord {a : Cardinal.{u_1}} : Ordinal.omega0 ≤ a.ord ↔ Cardinal.aleph0 ≤ a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

Equations

• Cardinal.ord.orderEmbedding = (RelEmbedding.ofMonotone Cardinal.ord Cardinal.ord.orderEmbedding.proof_2).orderEmbeddingOfLTEmbedding

@[simp]

theorem Cardinal.ord.orderEmbedding_coe : ⇑Cardinal.ord.orderEmbedding = Cardinal.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).

Equations

• Cardinal.univ.{?u.4, ?u.3} = Cardinal.lift.{?u.3, ?u.4 + 1} (Cardinal.mk Ordinal.{?u.4})

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

@[simp]

theorem Ordinal.card_univ : Ordinal.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 ↔ Ordinal.omega0 ≤ o

@[simp]

theorem Ordinal.card_lt_aleph0 {o : Ordinal.{u_1}} : o.card < Cardinal.aleph0 ↔ o < Ordinal.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 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 Ordinal.lift.{v, u}

@[deprecated Ordinal.mem_range_lift_of_card_le (since := "2024-10-07")]

theorem Ordinal.lift_down' {a : Cardinal.{u}} {b : Ordinal.{max u v}} (h : b.card ≤ Cardinal.lift.{v, u} a) : ∃ (a' : Ordinal.{u}), Ordinal.lift.{v, u} a' = b

@[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 α] : Ordinal.type r = ↑(Fintype.card α)

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

Sorted lists

theorem List.Sorted.lt_ord_of_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] {l m : List α} {o : Ordinal.{u}} (hl : List.Sorted (fun (x1 x2 : α) => x1 > x2) l) (hm : List.Sorted (fun (x1 x2 : α) => x1 > x2) m) (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