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

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

def Ordinal.IsLimit (o : Ordinal.{u_4}) : Prop

A limit ordinal is an ordinal which is not zero and not a successor.

Deprecated: use Order.IsSuccLimit instead.

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.not_isSuccLimit_succ (since := "2025-07-09")]

theorem Ordinal.not_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a

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

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

theorem Ordinal.IsLimit.pos {o : Ordinal.{u_4}} (h : o.IsLimit) : 0 < o

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

theorem Ordinal.IsLimit.ne_zero {o : Ordinal.{u_4}} (h : o.IsLimit) : o ≠ 0

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 Ordinal.zero_or_succ_or_isSuccLimit (since := "2025-07-09")]

theorem Ordinal.zero_or_succ_or_limit (o : Ordinal.{u_4}) : o = 0 ∨ (∃ (a : Ordinal.{u_4}), o = Order.succ a) ∨ o.IsLimit

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

theorem Ordinal.isLimit_of_not_succ_of_ne_zero {o : Ordinal.{u_4}} (h : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a) (h' : o ≠ 0) : o.IsLimit

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

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

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

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

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

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

@[deprecated Ordinal.pred_le_iff_le_succ (since := "2025-02-11")]

theorem Ordinal.pred_le {a b : Ordinal.{u_4}} : a.pred ≤ b ↔ a ≤ Order.succ b

Alias of Ordinal.pred_le_iff_le_succ.

@[simp]

theorem Ordinal.lt_pred_iff_succ_lt {a b : Ordinal.{u_4}} : a < b.pred ↔ Order.succ a < b

@[deprecated Ordinal.lt_pred_iff_succ_lt (since := "2025-02-11")]

theorem Ordinal.lt_pred {a b : Ordinal.{u_4}} : a < b.pred ↔ Order.succ a < b

Alias of Ordinal.lt_pred_iff_succ_lt.

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

def Ordinal.pred_succ_gi : GaloisInsertion pred Order.succ

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

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

@[deprecated Ordinal.pred_eq_iff_isSuccPrelimit (since := "2025-02-11")]

theorem Ordinal.pred_eq_iff_not_succ {o : Ordinal.{u_4}} : o.pred = o ↔ ¬∃ (a : Ordinal.{u_4}), o = Order.succ a

@[deprecated Ordinal.pred_eq_iff_isSuccPrelimit (since := "2025-02-11")]

theorem Ordinal.pred_eq_iff_not_succ' {o : Ordinal.{u_4}} : o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ Order.succ a

theorem Ordinal.pred_lt_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} : o.pred < o ↔ ¬Order.IsSuccPrelimit o

@[deprecated Ordinal.pred_lt_iff_not_isSuccPrelimit (since := "2025-02-11")]

theorem Ordinal.pred_lt_iff_is_succ {o : Ordinal.{u_4}} : o.pred < o ↔ ∃ (a : Ordinal.{u_4}), o = Order.succ a

theorem Ordinal.succ_pred_eq_iff_not_isSuccPrelimit {o : Ordinal.{u_4}} : Order.succ o.pred = o ↔ ¬Order.IsSuccPrelimit o

@[deprecated Ordinal.succ_pred_iff_is_succ (since := "2025-02-11")]

theorem Ordinal.succ_pred_iff_is_succ {o : Ordinal.{u_4}} : Order.succ o.pred = o ↔ ∃ (a : Ordinal.{u_4}), o = Order.succ a

@[deprecated Order.IsSuccPrelimit.succ_lt_iff (since := "2025-02-11")]

theorem Ordinal.succ_lt_of_not_succ {o b : Ordinal.{u_4}} (h : ¬∃ (a : Ordinal.{u_4}), o = Order.succ a) : Order.succ b < o ↔ b < o

@[deprecated Ordinal.isSuccPrelimit_lift (since := "2025-02-11")]

theorem Ordinal.lift_is_succ {o : Ordinal.{v}} : (∃ (a : Ordinal.{max v u}), lift.{u, v} o = Order.succ a) ↔ ∃ (a : Ordinal.{v}), o = Order.succ a

@[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}) : Prop

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.

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

theorem Ordinal.IsNormal.monotone {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) : Monotone 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) : id ≤ 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 : IsNormal id

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.

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

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

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.

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

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

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

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

theorem Ordinal.mul_ne_zero {a b : Ordinal.{u_4}} : a ≠ 0 → b ≠ 0 → a * b ≠ 0

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

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.

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

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

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 : ℕ) : ↑n < omega0

theorem Ordinal.eq_nat_or_omega0_le (o : Ordinal.{u_4}) : (∃ (n : ℕ), o = ↑n) ∨ omega0 ≤ o

theorem Ordinal.omega0_pos : 0 < omega0

theorem Ordinal.omega0_ne_zero : omega0 ≠ 0

theorem Ordinal.one_lt_omega0 : 1 < 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) : omega0 ≤ 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) : omega0 ≤ 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