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:

• IsLimit 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}

@[deprecated add_left_cancel_iff (since := "2024-12-11")]

theorem Ordinal.add_left_cancel (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}} : a + b = a + c ↔ b = c

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

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.

Equations

• o.pred = if h : ∃ (a : Ordinal.{?u.2}), o = Order.succ a then Classical.choose h else o

@[simp]

theorem Ordinal.pred_succ (o : Ordinal.{u_4}) : (Order.succ o).pred = o

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

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_eq_iff_not_succ' {o : Ordinal.{u_4}} : o.pred = o ↔ ∀ (a : Ordinal.{u_4}), o ≠ Order.succ a

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

@[simp]

theorem Ordinal.pred_zero : pred 0 = 0

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

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

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

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

@[simp]

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

Limit ordinals

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

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

TODO: deprecate this in favor of Order.IsSuccLimit.

Equations

• o.IsLimit = Order.IsSuccLimit o

theorem Ordinal.isLimit_iff {o : Ordinal.{u_4}} : o.IsLimit ↔ o ≠ 0 ∧ Order.IsSuccPrelimit o

theorem Ordinal.IsLimit.isSuccPrelimit {o : Ordinal.{u_4}} (h : o.IsLimit) : Order.IsSuccPrelimit o

theorem Ordinal.IsLimit.succ_lt {o a : Ordinal.{u_4}} (h : o.IsLimit) : a < o → Order.succ a < o

theorem Ordinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0

theorem Ordinal.not_zero_isLimit : ¬IsLimit 0

theorem Ordinal.not_succ_isLimit (o : Ordinal.{u_4}) : ¬(Order.succ o).IsLimit

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

theorem Ordinal.succ_lt_of_isLimit {o a : Ordinal.{u_4}} (h : o.IsLimit) : Order.succ a < o ↔ a < o

theorem Ordinal.le_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : o ≤ Order.succ a ↔ o ≤ a

theorem Ordinal.limit_le {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : o ≤ a ↔ ∀ x < o, x ≤ a

theorem Ordinal.lt_limit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} : a < o ↔ ∃ x < o, a < x

@[simp]

theorem Ordinal.lift_isLimit (o : Ordinal.{v}) : (lift.{u, v} o).IsLimit ↔ o.IsLimit

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

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

theorem Ordinal.IsLimit.one_lt {o : Ordinal.{u_4}} (h : o.IsLimit) : 1 < o

theorem Ordinal.IsLimit.nat_lt {o : Ordinal.{u_4}} (h : o.IsLimit) (n : ℕ) : ↑n < o

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

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

theorem Ordinal.IsLimit.sSup_Iio {o : Ordinal.{u_4}} (h : o.IsLimit) : sSup (Set.Iio o) = o

theorem Ordinal.IsLimit.iSup_Iio {o : Ordinal.{u_4}} (h : o.IsLimit) : ⨆ (a : ↑(Set.Iio o)), ↑a = o

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)) (isLimit : (o : Ordinal.{u_5}) → o.IsLimit → ((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 isLimit = SuccOrder.limitRecOn o (fun (a : Ordinal.{?u.61}) (ha : IsMin a) => ⋯.mpr zero) (fun (a : Ordinal.{?u.61}) (x : ¬IsMax a) => succ a) isLimit

@[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}) → o.IsLimit → ((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}) → o.IsLimit → ((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}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) (h : o.IsLimit) : 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 : l.IsLimit) {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, ⋯⟩) (isLimit : (o : ↑(Set.Iio l)) → (↑o).IsLimit → ((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.

@[simp]

theorem Ordinal.boundedLimitRec_zero {l : Ordinal.{u_4}} (lLim : l.IsLimit) {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)) → (↑o).IsLimit → ((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 : l.IsLimit) {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)) → (↑o).IsLimit → ((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 : l.IsLimit) {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)) → (↑o).IsLimit → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) (oLim : (↑o).IsLimit) : 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 : (type r).IsLimit) (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

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.

Equations

• Ordinal.IsNormal f = ((∀ (o : Ordinal.{?u.17}), f o < f (Order.succ o)) ∧ ∀ (o : Ordinal.{?u.17}), o.IsLimit → ∀ (a : Ordinal.{?u.16}), f o ≤ a ↔ ∀ b < o, f b ≤ a)

theorem Ordinal.IsNormal.limit_le {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {o : Ordinal.{u_4}} : o.IsLimit → ∀ {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 : o.IsLimit) {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}), o.IsLimit → ∀ (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.isLimit {f : Ordinal.{u_4} → Ordinal.{u_5}} (H : IsNormal f) {o : Ordinal.{u_4}} (ho : o.IsLimit) : (f o).IsLimit

theorem Ordinal.add_le_of_limit {a b c : Ordinal.{u_4}} (h : b.IsLimit) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c

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

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

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

Alias of Ordinal.isLimit_add.

Subtraction on ordinals

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.5}) => sInf {o : Ordinal.{?u.5} | a ≤ b + o} }

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.add_sub_cancel (a b : Ordinal.{u_4}) : a + b - 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.add_sub_cancel_of_le {a b : Ordinal.{u_4}} (h : b ≤ a) : b + (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

instance Ordinal.existsAddOfLE : ExistsAddOfLE Ordinal.{u_4}

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

@[deprecated Ordinal.add_le_iff (since := "2024-12-08")]

theorem Ordinal.add_le_of_forall_add_lt {a b c : Ordinal.{u_4}} (hb : 0 < b) (h : ∀ d < b, a + d < c) : a + b ≤ c

theorem Ordinal.isLimit_sub {a b : Ordinal.{u_4}} (ha : a.IsLimit) (h : b < a) : (a - b).IsLimit

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_of_limit {a b c : Ordinal.{u_4}} (h : b.IsLimit) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

theorem Ordinal.isNormal_mul_right {a : Ordinal.{u_4}} (h : 0 < a) : IsNormal fun (x : Ordinal.{u_4}) => a * x

theorem Ordinal.lt_mul_of_limit {a b c : Ordinal.{u_4}} (h : c.IsLimit) : a < b * c ↔ ∃ c' < c, a < b * c'

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.isLimit_mul {a b : Ordinal.{u_4}} (a0 : 0 < a) : b.IsLimit → (a * b).IsLimit

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

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_limit {a b c : Ordinal.{u_4}} (ba : b + a = a) (l : c.IsLimit) : (a + b) * c = a * c

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.isLimit_add_iff {a b : Ordinal.{u_4}} : (a + b).IsLimit ↔ b.IsLimit ∨ b = 0 ∧ a.IsLimit

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

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.isLimit_omega0 : omega0.IsLimit

theorem Ordinal.omega0_le {o : Ordinal.{u_4}} : omega0 ≤ o ↔ ∀ (n : ℕ), ↑n ≤ o

theorem Ordinal.nat_lt_limit {o : Ordinal.{u_4}} (h : o.IsLimit) (n : ℕ) : ↑n < o

theorem Ordinal.omega0_le_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) : omega0 ≤ 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.isLimit_iff_omega0_dvd {a : Ordinal.{u_4}} : a.IsLimit ↔ 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.isLimit_ord {c : Cardinal.{u_1}} (co : aleph0 ≤ c) : c.ord.IsLimit

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