Documentation

Mathlib.SetTheory.Ordinal.Arithmetic

Ordinal arithmetic #

Ordinals have an addition (corresponding to the 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 (truncated) subtraction and division operators.

Ordinal powers and logarithms are defined in Mathlib.SetTheory.Ordinal.Exponential.

Main definitions and results #

a + b is the order type of the lexicographic sum a ⊕ₗ b.
a - b is the unique ordinal c such that b + c = a, when b ≤ a.
a * b is the order type of the lexicographic product b ×ₗ a.
a / b is the ordinal q such that a = b * q + r with r < b. We also define the divisibility predicate, and a modulo operation.
limitRecOn is limit recursion on ordinals, i.e. well-founded recursion separating out the zero, successor, and limit cases.

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

Note that some basic functions and properties of ordinals have been generalized to other orders, and exist on other files:

Order.succ o = o + 1 is the successor of o.
Order.IsSuccLimit o: an ordinal is a limit ordinal if it is neither 0 nor a successor.
Order.IsNormal: a function f : Ordinal → Ordinal is normal if it is strictly increasing and order-continuous, i.e., the image f o of a limit ordinal o is the supremum 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

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

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

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

@[simp]

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

@[simp]

theorem Ordinal.isSuccPrelimit_zero :

Order.IsSuccPrelimit 0

@[simp]

theorem Ordinal.not_isSuccLimit_zero :

¬Order.IsSuccLimit 0

@[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

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

↑n < o

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

1 < o

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

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

noncomputable 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

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

Note that this is just a special (though sometimes convenient) case of the more general well-founded recursion WellFoundedLT.fix.

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₃

@[deprecated Ordinal.limitRecOn (since := "2025-12-26")]

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

Instances For

@[deprecated Ordinal.limitRecOn_zero (since := "2025-12-26")]

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₁

@[deprecated Ordinal.limitRecOn_succ (since := "2025-12-26")]

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₃)

@[deprecated Ordinal.limitRecOn_limit (since := "2025-12-26")]

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₃

@[implicit_reducible]

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

OrderTop (Order.succ o).ToType

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 #

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

The ordinal predecessor of a is b if a = succ b, and a otherwise.

Instances For

@[simp]

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

(o + 1).pred = o

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}) :

noncomputable def Ordinal.pred_succ_gi :

GaloisInsertion pred Order.succ

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

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

@[deprecated Order.IsNormal (since := "2025-12-25")]

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.

Instances For

@[deprecated Order.IsNormal.le_iff_forall_le (since := "2025-12-25")]

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

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

@[deprecated Order.IsNormal.lt_iff_exists_lt (since := "2025-12-25")]

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

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

@[deprecated Order.IsNormal.strictMono (since := "2025-12-25")]

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

@[deprecated Order.IsNormal.strictMono (since := "2025-12-25")]

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

@[deprecated Order.isNormal_iff (since := "2025-12-25")]

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

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

@[deprecated StrictMono.lt_iff_lt (since := "2025-12-25")]

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

f a < f b ↔ a < b

@[deprecated StrictMono.le_iff_le (since := "2025-12-25")]

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

f a ≤ f b ↔ a ≤ b

@[deprecated Function.Injective.eq_iff (since := "2025-12-25")]

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

f a = f b ↔ a = b

@[deprecated StrictMono.id_le (since := "2025-12-25")]

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

id ≤ f

@[deprecated StrictMono.le_apply (since := "2025-12-25")]

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

a ≤ f a

@[deprecated StrictMono.le_apply (since := "2025-12-25")]

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

f a ≤ a ↔ f a = a

@[deprecated Order.IsNormal.map_isLUB (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_set {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.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

@[deprecated Order.IsNormal.map_isLUB (since := "2025-12-25")]

theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : Ordinal.{u_4} → Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.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

@[deprecated Order.IsNormal.id (since := "2025-12-25")]

theorem Ordinal.IsNormal.refl :

Ordinal.IsNormal id

@[deprecated Order.IsNormal.comp (since := "2025-12-25")]

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

Order.IsNormal (f ∘ g)

@[deprecated Order.IsNormal.map_isSuccLimit (since := "2025-12-25")]

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

Order.IsSuccLimit (f o)

Subtraction on ordinals #

@[implicit_reducible]

noncomputable instance Ordinal.sub :

Sub Ordinal.{u_4}

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

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

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

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

Order.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)

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

Order.IsSuccLimit (a - b)

Multiplication of ordinals #

@[implicit_reducible]

instance Ordinal.monoid :

Monoid Ordinal.{u}

The multiplication of ordinals a and b is the order type of the lexicographic order on b × a.

@[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

@[implicit_reducible]

instance Ordinal.monoidWithZero :

MonoidWithZero Ordinal.{u_4}

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_4}

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

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

Order.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'

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

a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

instance Ordinal.instPosMulStrictMono :

PosMulStrictMono Ordinal.{u_4}

instance Ordinal.instIsLeftCancelMulZero :

IsLeftCancelMulZero Ordinal.{u_4}

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

Order.IsSuccLimit (a * b)

@[deprecated Ordinal.isSuccLimit_mul_right (since := "2026-02-01")]

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

Order.IsSuccLimit (a * b)

Alias of Ordinal.isSuccLimit_mul_right.

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

Order.IsSuccPrelimit (a * b)

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

Order.IsSuccLimit (a * b)

theorem Ordinal.isSuccPrelimit_mul_left {a b : Ordinal.{u_4}} (ha : Order.IsSuccLimit a) :

Order.IsSuccPrelimit (a * b)

@[simp]

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

n • a = a * ↑n

@[deprecated Ordinal.nsmul_eq_mul (since := "2026-03-14")]

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

n • a = a * ↑n

Alias of Ordinal.nsmul_eq_mul.

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

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

o * 2 = o + o

Division on ordinals #

@[implicit_reducible]

noncomputable instance Ordinal.div :

Div Ordinal.{u_4}

a / b is the unique ordinal q satisfying a = b * q + r with r < b.

@[simp]

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

a / 0 = 0

theorem Ordinal.mul_div_gc {a : Ordinal.{u_4}} (ha : a ≠ 0) :

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

Multiplication and division by a non-zero ordinal form a Galois connection.

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

a * b ≤ c ↔ b ≤ c / a

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

c < a * b ↔ c / a < b

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

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

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

a ≤ b / c ↔ c * a ≤ b

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

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

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.antisymm :

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

@[implicit_reducible]

noncomputable instance Ordinal.mod :

Mod Ordinal.{u_4}

a % b is the unique ordinal r satisfying a = b * q + r with r < 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

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

a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

theorem Ordinal.forall_lt_mul {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop} :

(∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

theorem Ordinal.exists_lt_mul {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop} :

(∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

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

@[simp]

theorem Ordinal.typein_lt_nat (x : ℕ) :

(typein LT.lt).toRelEmbedding x = ↑x

@[simp]

theorem Ordinal.typein_lt_fin {n : ℕ} (x : Fin n) :

(typein LT.lt).toRelEmbedding x = ↑↑x

@[simp]

theorem Ordinal.enum_lt_fin {n : ℕ} (x : Fin n) :

(enum LT.lt) ⟨↑↑x, ⋯⟩ = x

Properties of `ω` #

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

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

@[simp]

theorem Ordinal.natCast_lt_omega0 (n : ℕ) :

@[deprecated Ordinal.natCast_lt_omega0 (since := "2026-03-08")]

theorem Ordinal.nat_lt_omega0 (n : ℕ) :

Alias of Ordinal.natCast_lt_omega0.

@[simp]

theorem Ordinal.enum_lt_nat (x : ℕ) :

(enum LT.lt) ⟨↑x, ⋯⟩ = x

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 :

omega0 ≠ 0

@[simp]

theorem Ordinal.one_lt_omega0 :

theorem Ordinal.isSuccLimit_omega0 :

Order.IsSuccLimit omega0

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) :

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.isSuccPrelimit_iff_omega0_dvd {a : Ordinal.{u_4}} :

Order.IsSuccPrelimit a ↔ omega0 ∣ a

@[deprecated Ordinal.isSuccPrelimit_iff_omega0_dvd (since := "2026-02-01")]

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

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

@[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}} (hc : aleph0 ≤ c) :

Order.IsSuccLimit c.ord

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

NoMaxOrder c.ord.ToType