Documentation

Mathlib.SetTheory.Ordinal.Arithmetic

Ordinal arithmetic #

Ordinals have an addition (corresponding to disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define correspondingly a subtraction, a division, a successor function, a power function and a logarithm function.

We also define limit ordinals and prove the basic induction principle on ordinals separating successor ordinals and limit ordinals, in limitRecOn.

Main definitions and results #

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₂.
o₁ - o₂ is the unique ordinal o such that o₂ + o = o₁, when o₂ ≤ o₁.
o₁ * o₂ is the lexicographic order on o₂ × o₁.
o₁ / o₂ is the ordinal o such that o₁ = o₂ * o + o' with o' < o₂. We also define the divisibility predicate, and a modulo operation.
Order.succ o = o + 1 is the successor of o.
pred o if the predecessor of o. If o is not a successor, we set pred o = o.

We discuss the properties of casts of natural numbers of and of ω with respect to these operations.

Some properties of the operations are also used to discuss general tools on ordinals:

Order.IsSuccLimit o: an ordinal is a limit ordinal if it is neither 0 nor a successor.
limitRecOn is the main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.
IsNormal: a function f : Ordinal → Ordinal satisfies IsNormal if it is strictly increasing and order-continuous, i.e., the image f o of a limit ordinal o is the sup of f a for a < o.

Various other basic arithmetic results are given in Principal.lean instead.

Further properties of addition on ordinals #

@[simp]

theorem Ordinal.lift_add (a b : Ordinal.{v}) :

lift.{u, v} (a + b) = lift.{u, v} a + lift.{u, v} b

@[simp]

theorem Ordinal.lift_succ (a : Ordinal.{v}) :

lift.{u, v} (Order.succ a) = Order.succ (lift.{u, v} a)

instance Ordinal.instAddLeftReflectLE :

AddLeftReflectLE Ordinal.{u}

instance Ordinal.instIsLeftCancelAdd :

IsLeftCancelAdd Ordinal.{u_4}

instance Ordinal.instAddLeftStrictMono :

AddLeftStrictMono Ordinal.{u}

instance Ordinal.instAddLeftReflectLT :

AddLeftReflectLT Ordinal.{u}

instance Ordinal.instAddRightReflectLT :

AddRightReflectLT Ordinal.{u}

theorem Ordinal.add_le_add_iff_right {a b : Ordinal.{u_4}} (n : ℕ) :

a + ↑n ≤ b + ↑n ↔ a ≤ b

theorem Ordinal.add_right_cancel {a b : Ordinal.{u_4}} (n : ℕ) :

a + ↑n = b + ↑n ↔ a = b

theorem Ordinal.add_eq_zero_iff {a b : Ordinal.{u_4}} :

a + b = 0 ↔ a = 0 ∧ b = 0

theorem Ordinal.left_eq_zero_of_add_eq_zero {a b : Ordinal.{u_4}} (h : a + b = 0) :

a = 0

theorem Ordinal.right_eq_zero_of_add_eq_zero {a b : Ordinal.{u_4}} (h : a + b = 0) :

b = 0

Limit ordinals #

theorem Ordinal.isSuccLimit_iff {o : Ordinal.{u_4}} :

Order.IsSuccLimit o ↔ o ≠ 0 ∧ Order.IsSuccPrelimit o

@[deprecated Ordinal.isSuccLimit_iff (since := "2025-07-09")]

theorem Ordinal.isLimit_iff {o : Ordinal.{u_4}} :

Order.IsSuccLimit o ↔ o ≠ 0 ∧ Order.IsSuccPrelimit o

Alias of Ordinal.isSuccLimit_iff.

@[deprecated Order.IsSuccLimit.isSuccPrelimit (since := "2025-07-09")]

theorem Ordinal.IsLimit.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] (h : Order.IsSuccLimit a) :

Order.IsSuccPrelimit a

Alias of Order.IsSuccLimit.isSuccPrelimit.

@[deprecated Order.IsSuccLimit.succ_lt (since := "2025-07-09")]

theorem Ordinal.IsLimit.succ_lt {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) (ha : a < b) :

Order.succ a < b

Alias of Order.IsSuccLimit.succ_lt.

@[simp]

theorem Ordinal.isSuccPrelimit_zero :

Order.IsSuccPrelimit 0

@[simp]

theorem Ordinal.not_isSuccLimit_zero :

¬Order.IsSuccLimit 0

@[deprecated Ordinal.not_isSuccLimit_zero (since := "2025-07-09")]

theorem Ordinal.not_zero_isLimit :

¬Order.IsSuccLimit 0

Alias of Ordinal.not_isSuccLimit_zero.

@[deprecated Order.not_isSuccLimit_succ (since := "2025-07-09")]

theorem Ordinal.not_succ_isLimit {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :

¬Order.IsSuccLimit (Order.succ a)

Alias of Order.not_isSuccLimit_succ.

@[deprecated Order.IsSuccLimit.succ_lt_iff (since := "2025-07-09")]

theorem Ordinal.succ_lt_of_isLimit {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) :

Order.succ a < b ↔ a < b

Alias of Order.IsSuccLimit.succ_lt_iff.

@[deprecated Order.IsSuccLimit.le_succ_iff (since := "2025-07-09")]

theorem Ordinal.le_succ_of_isLimit {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) :

b ≤ Order.succ a ↔ b ≤ a

Alias of Order.IsSuccLimit.le_succ_iff.

@[deprecated Order.IsSuccLimit.le_iff_forall_le (since := "2025-07-09")]

theorem Ordinal.limit_le {α : Type u_1} {a b : α} [LinearOrder α] (h : Order.IsSuccLimit a) :

a ≤ b ↔ ∀ c < a, c ≤ b

Alias of Order.IsSuccLimit.le_iff_forall_le.

@[deprecated Order.IsSuccLimit.lt_iff_exists_lt (since := "2025-07-09")]

theorem Ordinal.lt_limit {α : Type u_1} {a b : α} [LinearOrder α] (h : Order.IsSuccLimit b) :

a < b ↔ ∃ c < b, a < c

Alias of Order.IsSuccLimit.lt_iff_exists_lt.

@[simp]

theorem Ordinal.isSuccPrelimit_lift {o : Ordinal.{v}} :

Order.IsSuccPrelimit (lift.{u, v} o) ↔ Order.IsSuccPrelimit o

@[simp]

theorem Ordinal.isSuccLimit_lift {o : Ordinal.{v}} :

Order.IsSuccLimit (lift.{u, v} o) ↔ Order.IsSuccLimit o

@[deprecated Ordinal.isSuccLimit_lift (since := "2025-07-09")]

theorem Ordinal.lift_isLimit {o : Ordinal.{v}} :

Order.IsSuccLimit (lift.{u, v} o) ↔ Order.IsSuccLimit o

Alias of Ordinal.isSuccLimit_lift.

theorem Ordinal.natCast_lt_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) (n : ℕ) :

↑n < o

@[deprecated Ordinal.natCast_lt_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.IsLimit.nat_lt {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) (n : ℕ) :

↑n < o

Alias of Ordinal.natCast_lt_of_isSuccLimit.

theorem Ordinal.one_lt_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) :

1 < o

@[deprecated Ordinal.one_lt_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.IsLimit.one_lt {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) :

1 < o

Alias of Ordinal.one_lt_of_isSuccLimit.

theorem Ordinal.zero_or_succ_or_isSuccLimit (o : Ordinal.{u_4}) :

o = 0 ∨ o ∈ Set.range Order.succ ∨ Order.IsSuccLimit o

@[deprecated Order.IsSuccLimit.sSup_Iio (since := "2025-07-09")]

theorem Ordinal.IsLimit.sSup_Iio {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {x : α} (h : Order.IsSuccLimit x) :

sSup (Set.Iio x) = x

Alias of Order.IsSuccLimit.sSup_Iio.

@[deprecated Order.IsSuccLimit.iSup_Iio (since := "2025-07-09")]

theorem Ordinal.IsLimit.iSup_Iio {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {x : α} (h : Order.IsSuccLimit x) :

⨆ (a : ↑(Set.Iio x)), ↑a = x

Alias of Order.IsSuccLimit.iSup_Iio.

def Ordinal.limitRecOn {motive : Ordinal.{u_5} → Sort u_4} (o : Ordinal.{u_5}) (zero : motive 0) (succ : (o : Ordinal.{u_5}) → motive o → motive (Order.succ o)) (limit : (o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) :

motive o

Main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.

Equations

Ordinal.limitRecOn o zero succ limit = SuccOrder.limitRecOn o (fun (_a : Ordinal.{?u.78}) (ha : IsMin _a) => ⋯ ▸ zero) (fun (a : Ordinal.{?u.78}) (x : ¬IsMax a) => succ a) limit

Instances For

@[simp]

theorem Ordinal.limitRecOn_zero {motive : Ordinal.{u_4} → Sort u_5} (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) :

limitRecOn 0 H₁ H₂ H₃ = H₁

@[simp]

theorem Ordinal.limitRecOn_succ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) :

limitRecOn (Order.succ o) H₁ H₂ H₃ = H₂ o (limitRecOn o H₁ H₂ H₃)

@[simp]

theorem Ordinal.limitRecOn_limit {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) (h : Order.IsSuccLimit o) :

limitRecOn o H₁ H₂ H₃ = H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) => limitRecOn x H₁ H₂ H₃

def Ordinal.boundedLimitRecOn {l : Ordinal.{u_5}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_4} (o : ↑(Set.Iio l)) (zero : motive ⟨0, ⋯⟩) (succ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (limit : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) :

motive o

Bounded recursion on ordinals. Similar to limitRecOn, with the assumption o < l added to all cases. The final term's domain is the ordinals below l.

Equations

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

Instances For

@[simp]

theorem Ordinal.boundedLimitRec_zero {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) :

boundedLimitRecOn lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁

@[simp]

theorem Ordinal.boundedLimitRec_succ {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) :

boundedLimitRecOn lLim ⟨Order.succ ↑o, ⋯⟩ H₁ H₂ H₃ = H₂ o (boundedLimitRecOn lLim o H₁ H₂ H₃)

theorem Ordinal.boundedLimitRec_limit {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) (oLim : Order.IsSuccLimit ↑o) :

boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun (x : ↑(Set.Iio l)) (x_1 : x < o) => boundedLimitRecOn lLim x H₁ H₂ H₃

instance Ordinal.orderTopToTypeSucc (o : Ordinal.{u_4}) :

OrderTop (Order.succ o).toType

Equations

o.orderTopToTypeSucc = { top := (Ordinal.enum fun (x1 x2 : (Order.succ o).toType) => x1 < x2).toRelEmbedding ⟨o, ⋯⟩, le_top := ⋯ }

theorem Ordinal.enum_succ_eq_top {o : Ordinal.{u_4}} :

(enum fun (x1 x2 : (Order.succ o).toType) => x1 < x2) ⟨o, ⋯⟩ = ⊤

theorem Ordinal.has_succ_of_type_succ_lt {α : Type u_4} {r : α → α → Prop} [wo : IsWellOrder α r] (h : ∀ a < type r, Order.succ a < type r) (x : α) :

∃ (y : α), r x y

theorem Ordinal.toType_noMax_of_succ_lt {o : Ordinal.{u_4}} (ho : ∀ a < o, Order.succ a < o) :

NoMaxOrder o.toType

theorem Ordinal.bounded_singleton {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (hr : Order.IsSuccLimit (type r)) (x : α) :

Set.Bounded r {x}

@[simp]

theorem Ordinal.typein_ordinal (o : Ordinal.{u}) :

(typein fun (x1 x2 : Ordinal.{u}) => x1 < x2).toRelEmbedding o = lift.{u + 1, u} o

theorem Ordinal.mk_Iio_ordinal (o : Ordinal.{u}) :

Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card

The predecessor of an ordinal #

def Ordinal.pred (o : Ordinal.{u_4}) :

The ordinal predecessor of o is o' if o = succ o', and o otherwise.

Equations

o.pred = Order.isSuccPrelimitRecOn o (fun (a : Ordinal.{?u.11}) (x : ¬IsMax a) => a) fun (a : Ordinal.{?u.11}) (x : Order.IsSuccPrelimit a) => a

Instances For

@[simp]

theorem Ordinal.pred_succ (o : Ordinal.{u_4}) :

(Order.succ o).pred = o

theorem Ordinal.pred_eq_of_isSuccPrelimit {o : Ordinal.{u_4}} :

Order.IsSuccPrelimit o → o.pred = o

theorem Order.IsSuccPrelimit.ordinalPred_eq {o : Ordinal.{u_4}} :

IsSuccPrelimit o → o.pred = o

Alias of Ordinal.pred_eq_of_isSuccPrelimit.

theorem Order.IsSuccLimit.ordinalPred_eq {o : Ordinal.{u_4}} (ho : IsSuccLimit o) :

o.pred = o

@[simp]

theorem Ordinal.pred_zero :

pred 0 = 0

@[simp]

theorem Ordinal.pred_le_iff_le_succ {a b : Ordinal.{u_4}} :

a.pred ≤ b ↔ a ≤ Order.succ b

@[simp]

theorem Ordinal.lt_pred_iff_succ_lt {a b : Ordinal.{u_4}} :

a < b.pred ↔ Order.succ a < b

theorem Ordinal.pred_le_self (o : Ordinal.{u_4}) :

def Ordinal.pred_succ_gi :

GaloisInsertion pred Order.succ

Ordinal.pred and Order.succ form a Galois insertion.

Equations

Ordinal.pred_succ_gi = GaloisConnection.toGaloisInsertion (@Ordinal.pred_le_iff_le_succ) Ordinal.pred_succ_gi._proof_1

Instances For

theorem Ordinal.pred_surjective :

Function.Surjective pred

theorem Ordinal.self_le_succ_pred (o : Ordinal.{u_4}) :

o ≤ Order.succ o.pred

theorem Ordinal.pred_eq_iff_isSuccPrelimit {o : Ordinal.{u_4}} :

o.pred = o ↔ Order.IsSuccPrelimit o

theorem Ordinal.pred_lt_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} :

o.pred < o ↔ ¬Order.IsSuccPrelimit o

theorem Ordinal.succ_pred_eq_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} :

Order.succ o.pred = o ↔ ¬Order.IsSuccPrelimit o

@[simp]

theorem Ordinal.lift_pred (o : Ordinal.{v}) :

lift.{u, v} o.pred = (lift.{u, v} o).pred

Normal ordinal functions #

def Ordinal.IsNormal (f : Ordinal.{u_4} → Ordinal.{u_5}) :

A normal ordinal function is a strictly increasing function which is order-continuous, i.e., the image f o of a limit ordinal o is the sup of f a for a < o.

Todo: deprecate this in favor of Order.IsNormal.

Equations

Ordinal.IsNormal f = Order.IsNormal f

Instances For

theorem Ordinal.IsNormal.limit_le {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {o : Ordinal.{u_4}} :

Order.IsSuccLimit o → ∀ {a : Ordinal.{u_5}}, f o ≤ a ↔ ∀ b < o, f b ≤ a

theorem Ordinal.IsNormal.limit_lt {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) {a : Ordinal.{u_5}} :

a < f o ↔ ∃ b < o, a < f b

theorem Ordinal.IsNormal.strictMono {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) :

theorem Ordinal.IsNormal.monotone {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) :

theorem Ordinal.isNormal_iff_strictMono_limit (f : Ordinal.{u_4} → Ordinal.{u_5}) :

IsNormal f ↔ StrictMono f ∧ ∀ (o : Ordinal.{u_4}), Order.IsSuccLimit o → ∀ (a : Ordinal.{u_5}), (∀ b < o, f b ≤ a) → f o ≤ a

theorem Ordinal.IsNormal.lt_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {a b : Ordinal.{u_4}} :

f a < f b ↔ a < b

theorem Ordinal.IsNormal.le_iff {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {a b : Ordinal.{u_4}} :

f a ≤ f b ↔ a ≤ b

theorem Ordinal.IsNormal.inj {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {a b : Ordinal.{u_4}} :

f a = f b ↔ a = b

theorem Ordinal.IsNormal.id_le {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : IsNormal f) :

theorem Ordinal.IsNormal.le_apply {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : IsNormal f) {a : Ordinal.{u_4}} :

a ≤ f a

theorem Ordinal.IsNormal.le_iff_eq {f : Ordinal.{u_4} → Ordinal.{u_4}} (H : IsNormal f) {a : Ordinal.{u_4}} :

f a ≤ a ↔ f a = a

theorem Ordinal.IsNormal.le_set {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : IsNormal f) (p : Set Ordinal.{u_4}) (p0 : p.Nonempty) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o) :

f b ≤ o ↔ ∀ a ∈ p, f a ≤ o

theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal.{u_4}) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o) :

f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

theorem Ordinal.IsNormal.refl :

theorem Ordinal.IsNormal.trans {f : Ordinal.{u_4} → Ordinal.{u_5}} {g : Ordinal.{u_6} → Ordinal.{u_4}} (H₁ : IsNormal f) (H₂ : IsNormal g) :

IsNormal (f ∘ g)

theorem Ordinal.IsNormal.isSuccLimit {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {o : Ordinal.{u_4}} (ho : Order.IsSuccLimit o) :

Order.IsSuccLimit (f o)

Subtraction on ordinals #

instance Ordinal.existsAddOfLE :

ExistsAddOfLE Ordinal.{u_4}

instance Ordinal.canonicallyOrderedAdd :

CanonicallyOrderedAdd Ordinal.{u_4}

instance Ordinal.sub :

Sub Ordinal.{u_4}

a - b is the unique ordinal satisfying b + (a - b) = a when b ≤ a.

Equations

Ordinal.sub = { sub := fun (a b : Ordinal.{?u.7}) => if h : b ≤ a then Classical.choose ⋯ else 0 }

theorem Ordinal.add_sub_cancel_of_le {a b : Ordinal.{u_4}} (h : b ≤ a) :

b + (a - b) = a

@[simp]

theorem Ordinal.add_sub_cancel (a b : Ordinal.{u_4}) :

a + b - a = b

theorem Ordinal.le_add_sub (a b : Ordinal.{u_4}) :

a ≤ b + (a - b)

theorem Ordinal.sub_le {a b c : Ordinal.{u_4}} :

a - b ≤ c ↔ a ≤ b + c

theorem Ordinal.lt_sub {a b c : Ordinal.{u_4}} :

a < b - c ↔ c + a < b

theorem Ordinal.sub_eq_of_add_eq {a b c : Ordinal.{u_4}} (h : a + b = c) :

c - a = b

theorem Ordinal.sub_le_self (a b : Ordinal.{u_4}) :

a - b ≤ a

theorem Ordinal.le_sub_of_le {a b c : Ordinal.{u_4}} (h : b ≤ a) :

c ≤ a - b ↔ b + c ≤ a

theorem Ordinal.sub_lt_of_le {a b c : Ordinal.{u_4}} (h : b ≤ a) :

a - b < c ↔ a < b + c

@[simp]

theorem Ordinal.sub_zero (a : Ordinal.{u_4}) :

a - 0 = a

@[simp]

theorem Ordinal.zero_sub (a : Ordinal.{u_4}) :

0 - a = 0

@[simp]

theorem Ordinal.sub_self (a : Ordinal.{u_4}) :

a - a = 0

theorem Ordinal.sub_eq_zero_iff_le {a b : Ordinal.{u_4}} :

a - b = 0 ↔ a ≤ b

theorem Ordinal.sub_ne_zero_iff_lt {a b : Ordinal.{u_4}} :

a - b ≠ 0 ↔ b < a

theorem Ordinal.sub_sub (a b c : Ordinal.{u_4}) :

a - b - c = a - (b + c)

@[simp]

theorem Ordinal.add_sub_add_cancel (a b c : Ordinal.{u_4}) :

a + b - (a + c) = b - c

theorem Ordinal.le_sub_of_add_le {a b c : Ordinal.{u_4}} (h : b + c ≤ a) :

c ≤ a - b

theorem Ordinal.sub_lt_of_lt_add {a b c : Ordinal.{u_4}} (h : a < b + c) (hc : 0 < c) :

a - b < c

theorem Ordinal.lt_add_iff {a b c : Ordinal.{u_4}} (hc : c ≠ 0) :

a < b + c ↔ ∃ d < c, a ≤ b + d

theorem Ordinal.add_le_iff {a b c : Ordinal.{u_4}} (hb : b ≠ 0) :

a + b ≤ c ↔ ∀ d < b, a + d < c

theorem Ordinal.lt_add_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (hc : Order.IsSuccLimit c) :

a < b + c ↔ ∃ d < c, a < b + d

@[deprecated Ordinal.lt_add_iff_of_isSuccLimit (since := "2025-07-08")]

theorem Ordinal.lt_add_of_limit {a b c : Ordinal.{u_4}} (hc : Order.IsSuccLimit c) :

a < b + c ↔ ∃ d < c, a < b + d

Alias of Ordinal.lt_add_iff_of_isSuccLimit.

theorem Ordinal.add_le_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) :

a + b ≤ c ↔ ∀ d < b, a + d ≤ c

@[deprecated Ordinal.add_le_iff_of_isSuccLimit (since := "2025-07-08")]

theorem Ordinal.add_le_of_limit {a b c : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) :

a + b ≤ c ↔ ∀ d < b, a + d ≤ c

Alias of Ordinal.add_le_iff_of_isSuccLimit.

theorem Ordinal.isNormal_add_right (a : Ordinal.{u_4}) :

IsNormal fun (x : Ordinal.{u_4}) => a + x

theorem Ordinal.isSuccLimit_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :

Order.IsSuccLimit b → Order.IsSuccLimit (a + b)

@[deprecated Ordinal.isSuccLimit_add (since := "2025-07-09")]

theorem Ordinal.isLimit_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :

Order.IsSuccLimit b → Order.IsSuccLimit (a + b)

Alias of Ordinal.isSuccLimit_add.

@[deprecated Ordinal.isSuccLimit_add (since := "2025-07-09")]

theorem Ordinal.IsLimit.add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :

Order.IsSuccLimit b → Order.IsSuccLimit (a + b)

Alias of Ordinal.isSuccLimit_add.

theorem Ordinal.isSuccLimit_sub {a b : Ordinal.{u_4}} (ha : Order.IsSuccLimit a) (h : b < a) :

Order.IsSuccLimit (a - b)

@[deprecated Ordinal.isSuccLimit_sub (since := "2025-07-09")]

theorem Ordinal.isLimit_sub {a b : Ordinal.{u_4}} (ha : Order.IsSuccLimit a) (h : b < a) :

Order.IsSuccLimit (a - b)

Alias of Ordinal.isSuccLimit_sub.

Multiplication of ordinals #

instance Ordinal.monoid :

Monoid Ordinal.{u}

The multiplication of ordinals o₁ and o₂ is the (well-founded) lexicographic order on o₂ × o₁.

Equations

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

@[simp]

theorem Ordinal.type_prod_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] :

type (Prod.Lex s r) = type r * type s

instance Ordinal.monoidWithZero :

MonoidWithZero Ordinal.{u_4}

Equations

Ordinal.monoidWithZero = { toMonoid := Ordinal.monoid, zero := 0, zero_mul := Ordinal.monoidWithZero._proof_1, mul_zero := Ordinal.monoidWithZero._proof_2 }

instance Ordinal.noZeroDivisors :

NoZeroDivisors Ordinal.{u_4}

@[simp]

theorem Ordinal.lift_mul (a b : Ordinal.{v}) :

lift.{u, v} (a * b) = lift.{u, v} a * lift.{u, v} b

@[simp]

theorem Ordinal.card_mul (a b : Ordinal.{u_4}) :

(a * b).card = a.card * b.card

instance Ordinal.leftDistribClass :

LeftDistribClass Ordinal.{u}

theorem Ordinal.mul_succ (a b : Ordinal.{u_4}) :

a * Order.succ b = a * b + a

instance Ordinal.mulLeftMono :

MulLeftMono Ordinal.{u}

instance Ordinal.mulRightMono :

MulRightMono Ordinal.{u}

theorem Ordinal.le_mul_left (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :

a ≤ a * b

theorem Ordinal.le_mul_right (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :

a ≤ b * a

theorem Ordinal.mul_le_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit b) :

a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

@[deprecated Ordinal.mul_le_iff_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.mul_le_of_limit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit b) :

a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Alias of Ordinal.mul_le_iff_of_isSuccLimit.

theorem Ordinal.isNormal_mul_right {a : Ordinal.{u_4}} (h : 0 < a) :

IsNormal fun (x : Ordinal.{u_4}) => a * x

theorem Ordinal.lt_mul_iff_of_isSuccLimit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit c) :

a < b * c ↔ ∃ c' < c, a < b * c'

@[deprecated Ordinal.lt_mul_iff_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.lt_mul_of_limit {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit c) :

a < b * c ↔ ∃ c' < c, a < b * c'

Alias of Ordinal.lt_mul_iff_of_isSuccLimit.

instance Ordinal.instPosMulStrictMono :

PosMulStrictMono Ordinal.{u_4}

@[deprecated mul_lt_mul_iff_right₀ (since := "2025-08-26")]

theorem Ordinal.mul_lt_mul_iff_left {a b c : Ordinal.{u_4}} (a0 : 0 < a) :

a * b < a * c ↔ b < c

@[deprecated mul_le_mul_left (since := "2025-08-26")]

theorem Ordinal.mul_le_mul_iff_left {a b c : Ordinal.{u_4}} (a0 : 0 < a) :

a * b ≤ a * c ↔ b ≤ c

@[deprecated mul_lt_mul_of_pos_left (since := "2025-08-26")]

theorem Ordinal.mul_lt_mul_of_pos_left {a b c : Ordinal.{u_4}} (h : a < b) (c0 : 0 < c) :

c * a < c * b

@[deprecated mul_pos (since := "2025-08-26")]

theorem Ordinal.mul_pos {a b : Ordinal.{u_4}} (h₁ : 0 < a) (h₂ : 0 < b) :

0 < a * b

@[deprecated mul_ne_zero (since := "2025-08-26")]

theorem Ordinal.mul_ne_zero {a b : Ordinal.{u_4}} (ha : a ≠ 0) (hb : b ≠ 0) :

a * b ≠ 0

@[deprecated mul_le_mul_left (since := "2025-08-26")]

theorem Ordinal.le_of_mul_le_mul_left {a b c : Ordinal.{u_4}} (h : c * a ≤ c * b) (h0 : 0 < c) :

a ≤ b

@[deprecated mul_left_cancel_iff_of_pos (since := "2025-08-26")]

theorem Ordinal.mul_right_inj {a b c : Ordinal.{u_4}} (a0 : 0 < a) :

a * b = a * c ↔ b = c

theorem Ordinal.isSuccLimit_mul {a b : Ordinal.{u_4}} (a0 : 0 < a) :

Order.IsSuccLimit b → Order.IsSuccLimit (a * b)

@[deprecated Ordinal.isSuccLimit_mul (since := "2025-07-09")]

theorem Ordinal.isLimit_mul {a b : Ordinal.{u_4}} (a0 : 0 < a) :

Order.IsSuccLimit b → Order.IsSuccLimit (a * b)

Alias of Ordinal.isSuccLimit_mul.

theorem Ordinal.isSuccLimit_mul_left {a b : Ordinal.{u_4}} (l : Order.IsSuccLimit a) (b0 : 0 < b) :

Order.IsSuccLimit (a * b)

@[deprecated Ordinal.isSuccLimit_mul_left (since := "2025-07-09")]

theorem Ordinal.isLimit_mul_left {a b : Ordinal.{u_4}} (l : Order.IsSuccLimit a) (b0 : 0 < b) :

Order.IsSuccLimit (a * b)

Alias of Ordinal.isSuccLimit_mul_left.

theorem Ordinal.smul_eq_mul (n : ℕ) (a : Ordinal.{u_4}) :

n • a = a * ↑n

theorem Ordinal.add_mul_succ {a b : Ordinal.{u_4}} (c : Ordinal.{u_4}) (ba : b + a = a) :

(a + b) * Order.succ c = a * Order.succ c + b

theorem Ordinal.add_mul_of_isSuccLimit {a b c : Ordinal.{u_4}} (ba : b + a = a) (l : Order.IsSuccLimit c) :

(a + b) * c = a * c

@[deprecated Ordinal.add_mul_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.add_mul_limit {a b c : Ordinal.{u_4}} (ba : b + a = a) (l : Order.IsSuccLimit c) :

(a + b) * c = a * c

Alias of Ordinal.add_mul_of_isSuccLimit.

Division on ordinals #

instance Ordinal.div :

Div Ordinal.{u_4}

a / b is the unique ordinal o satisfying a = b * o + o' with o' < b.

Equations

Ordinal.div = { div := fun (a b : Ordinal.{?u.5}) => if b = 0 then 0 else sInf {o : Ordinal.{?u.5} | a < b * Order.succ o} }

@[simp]

theorem Ordinal.div_zero (a : Ordinal.{u_4}) :

a / 0 = 0

theorem Ordinal.lt_mul_succ_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) :

a < b * Order.succ (a / b)

theorem Ordinal.lt_mul_div_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) :

a < b * (a / b) + b

theorem Ordinal.div_le {a b c : Ordinal.{u_4}} (b0 : b ≠ 0) :

a / b ≤ c ↔ a < b * Order.succ c

theorem Ordinal.lt_div {a b c : Ordinal.{u_4}} (h : c ≠ 0) :

a < b / c ↔ c * Order.succ a ≤ b

theorem Ordinal.div_pos {b c : Ordinal.{u_4}} (h : c ≠ 0) :

0 < b / c ↔ c ≤ b

theorem Ordinal.le_div {a b c : Ordinal.{u_4}} (c0 : c ≠ 0) :

a ≤ b / c ↔ c * a ≤ b

theorem Ordinal.div_lt {a b c : Ordinal.{u_4}} (b0 : b ≠ 0) :

a / b < c ↔ a < b * c

theorem Ordinal.div_le_of_le_mul {a b c : Ordinal.{u_4}} (h : a ≤ b * c) :

a / b ≤ c

theorem Ordinal.mul_lt_of_lt_div {a b c : Ordinal.{u_4}} :

a < b / c → c * a < b

@[simp]

theorem Ordinal.zero_div (a : Ordinal.{u_4}) :

0 / a = 0

theorem Ordinal.mul_div_le (a b : Ordinal.{u_4}) :

b * (a / b) ≤ a

theorem Ordinal.div_le_left {a b : Ordinal.{u_4}} (h : a ≤ b) (c : Ordinal.{u_4}) :

a / c ≤ b / c

theorem Ordinal.mul_add_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) (c : Ordinal.{u_4}) :

(b * a + c) / b = a + c / b

theorem Ordinal.div_eq_zero_of_lt {a b : Ordinal.{u_4}} (h : a < b) :

a / b = 0

@[simp]

theorem Ordinal.mul_div_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b ≠ 0) :

b * a / b = a

theorem Ordinal.mul_add_div_mul {a c : Ordinal.{u_4}} (hc : c < a) (b d : Ordinal.{u_4}) :

(a * b + c) / (a * d) = b / d

theorem Ordinal.mul_div_mul_cancel {a : Ordinal.{u_4}} (ha : a ≠ 0) (b c : Ordinal.{u_4}) :

a * b / (a * c) = b / c

@[simp]

theorem Ordinal.div_one (a : Ordinal.{u_4}) :

a / 1 = a

@[simp]

theorem Ordinal.div_self {a : Ordinal.{u_4}} (h : a ≠ 0) :

a / a = 1

theorem Ordinal.mul_sub (a b c : Ordinal.{u_4}) :

a * (b - c) = a * b - a * c

theorem Ordinal.isSuccLimit_add_iff {a b : Ordinal.{u_4}} :

Order.IsSuccLimit (a + b) ↔ Order.IsSuccLimit b ∨ b = 0 ∧ Order.IsSuccLimit a

theorem Ordinal.isSuccLimit_add_iff_of_isSuccLimit {a b : Ordinal.{u_4}} (h : Order.IsSuccLimit a) :

Order.IsSuccLimit (a + b) ↔ Order.IsSuccPrelimit b

@[deprecated Ordinal.isSuccLimit_add_iff (since := "2025-07-09")]

theorem Ordinal.isLimit_add_iff {a b : Ordinal.{u_4}} :

Order.IsSuccLimit (a + b) ↔ Order.IsSuccLimit b ∨ b = 0 ∧ Order.IsSuccLimit a

Alias of Ordinal.isSuccLimit_add_iff.

theorem Ordinal.dvd_add_iff {a b c : Ordinal.{u_4}} :

a ∣ b → (a ∣ b + c ↔ a ∣ c)

theorem Ordinal.div_mul_cancel {a b : Ordinal.{u_4}} :

a ≠ 0 → a ∣ b → a * (b / a) = b

theorem Ordinal.le_of_dvd {a b : Ordinal.{u_4}} :

b ≠ 0 → a ∣ b → a ≤ b

theorem Ordinal.dvd_antisymm {a b : Ordinal.{u_4}} (h₁ : a ∣ b) (h₂ : b ∣ a) :

a = b

instance Ordinal.isAntisymm :

IsAntisymm Ordinal.{u_4} fun (x1 x2 : Ordinal.{u_4}) => x1 ∣ x2

instance Ordinal.mod :

Mod Ordinal.{u_4}

a % b is the unique ordinal o' satisfying a = b * o + o' with o' < b.

Equations

Ordinal.mod = { mod := fun (a b : Ordinal.{?u.4}) => a - b * (a / b) }

theorem Ordinal.mod_def (a b : Ordinal.{u_4}) :

a % b = a - b * (a / b)

theorem Ordinal.mod_le (a b : Ordinal.{u_4}) :

a % b ≤ a

@[simp]

theorem Ordinal.mod_zero (a : Ordinal.{u_4}) :

a % 0 = a

theorem Ordinal.mod_eq_of_lt {a b : Ordinal.{u_4}} (h : a < b) :

a % b = a

@[simp]

theorem Ordinal.zero_mod (b : Ordinal.{u_4}) :

0 % b = 0

theorem Ordinal.div_add_mod (a b : Ordinal.{u_4}) :

b * (a / b) + a % b = a

theorem Ordinal.mod_lt (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) :

a % b < b

@[simp]

theorem Ordinal.mod_self (a : Ordinal.{u_4}) :

a % a = 0

@[simp]

theorem Ordinal.mod_one (a : Ordinal.{u_4}) :

a % 1 = 0

theorem Ordinal.dvd_of_mod_eq_zero {a b : Ordinal.{u_4}} (H : a % b = 0) :

b ∣ a

theorem Ordinal.mod_eq_zero_of_dvd {a b : Ordinal.{u_4}} (H : b ∣ a) :

a % b = 0

theorem Ordinal.dvd_iff_mod_eq_zero {a b : Ordinal.{u_4}} :

b ∣ a ↔ a % b = 0

@[simp]

theorem Ordinal.mul_add_mod_self (x y z : Ordinal.{u_4}) :

(x * y + z) % x = z % x

@[simp]

theorem Ordinal.mul_mod (x y : Ordinal.{u_4}) :

x * y % x = 0

theorem Ordinal.mul_add_mod_mul {w x : Ordinal.{u_4}} (hw : w < x) (y z : Ordinal.{u_4}) :

(x * y + w) % (x * z) = x * (y % z) + w

theorem Ordinal.mul_mod_mul (x y z : Ordinal.{u_4}) :

x * y % (x * z) = x * (y % z)

theorem Ordinal.mod_mod_of_dvd (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}} (h : c ∣ b) :

a % b % c = a % c

@[simp]

theorem Ordinal.mod_mod (a b : Ordinal.{u_4}) :

a % b % b = a % b

Casting naturals into ordinals, compatibility with operations #

instance Ordinal.instCharZero :

CharZero Ordinal.{u_4}

@[simp]

theorem Ordinal.one_add_natCast (m : ℕ) :

1 + ↑m = ↑(Order.succ m)

@[simp]

theorem Ordinal.one_add_ofNat (m : ℕ) [m.AtLeastTwo] :

1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)

@[simp]

theorem Ordinal.natCast_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

@[simp]

theorem Ordinal.natCast_sub (m n : ℕ) :

↑(m - n) = ↑m - ↑n

@[simp]

theorem Ordinal.natCast_div (m n : ℕ) :

↑(m / n) = ↑m / ↑n

@[simp]

theorem Ordinal.natCast_mod (m n : ℕ) :

↑(m % n) = ↑m % ↑n

@[simp]

theorem Ordinal.lift_natCast (n : ℕ) :

lift.{u, v} ↑n = ↑n

@[simp]

theorem Ordinal.lift_ofNat (n : ℕ) [n.AtLeastTwo] :

lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

Properties of `ω` #

theorem Ordinal.lt_omega0 {o : Ordinal.{u_4}} :

o < omega0 ↔ ∃ (n : ℕ), o = ↑n

theorem Ordinal.nat_lt_omega0 (n : ℕ) :

theorem Ordinal.eq_nat_or_omega0_le (o : Ordinal.{u_4}) :

(∃ (n : ℕ), o = ↑n) ∨ omega0 ≤ o

@[simp]

theorem Ordinal.omega0_pos :

@[simp]

theorem Ordinal.omega0_ne_zero :

@[simp]

theorem Ordinal.one_lt_omega0 :

theorem Ordinal.isSuccLimit_omega0 :

Order.IsSuccLimit omega0

@[deprecated Ordinal.isSuccLimit_omega0 (since := "2025-07-09")]

theorem Ordinal.isLimit_omega0 :

Order.IsSuccLimit omega0

Alias of Ordinal.isSuccLimit_omega0.

@[deprecated Ordinal.natCast_lt_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.nat_lt_limit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) (n : ℕ) :

↑n < o

Alias of Ordinal.natCast_lt_of_isSuccLimit.

theorem Ordinal.omega0_le {o : Ordinal.{u_4}} :

omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

theorem Ordinal.omega0_le_of_isSuccLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) :

@[deprecated Ordinal.omega0_le_of_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.omega0_le_of_isLimit {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) :

Alias of Ordinal.omega0_le_of_isSuccLimit.

theorem Ordinal.natCast_add_omega0 (n : ℕ) :

↑n + omega0 = omega0

theorem Ordinal.one_add_omega0 :

1 + omega0 = omega0

theorem Ordinal.add_omega0 {a : Ordinal.{u_4}} (h : a < omega0) :

a + omega0 = omega0

@[simp]

theorem Ordinal.natCast_add_of_omega0_le {o : Ordinal.{u_4}} (h : omega0 ≤ o) (n : ℕ) :

↑n + o = o

@[simp]

theorem Ordinal.one_add_of_omega0_le {o : Ordinal.{u_4}} (h : omega0 ≤ o) :

1 + o = o

theorem Ordinal.isSuccLimit_iff_omega0_dvd {a : Ordinal.{u_4}} :

Order.IsSuccLimit a ↔ a ≠ 0 ∧ omega0 ∣ a

@[deprecated Ordinal.isSuccLimit_iff_omega0_dvd (since := "2025-07-09")]

theorem Ordinal.isLimit_iff_omega0_dvd {a : Ordinal.{u_4}} :

Order.IsSuccLimit a ↔ a ≠ 0 ∧ omega0 ∣ a

Alias of Ordinal.isSuccLimit_iff_omega0_dvd.

@[simp]

theorem Ordinal.natCast_mod_omega0 (n : ℕ) :

↑n % omega0 = ↑n

@[simp]

theorem Cardinal.add_one_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :

c + 1 = c

theorem Cardinal.isSuccLimit_ord {c : Cardinal.{u_1}} (co : aleph0 ≤ c) :

Order.IsSuccLimit c.ord

@[deprecated Cardinal.isSuccLimit_ord (since := "2025-07-09")]

theorem Cardinal.isLimit_ord {c : Cardinal.{u_1}} (co : aleph0 ≤ c) :

Order.IsSuccLimit c.ord

Alias of Cardinal.isSuccLimit_ord.

theorem Cardinal.noMaxOrder {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :

NoMaxOrder c.ord.toType