mathlib documentation

set_theory.ordinal.natural_ops

Natural operations on ordinals #

The goal of this file is to define natural addition and multiplication on ordinals, also known as the Hessenberg sum and product, and provide a basic API. The natural addition of two ordinals a ♯ b is recursively defined as the least ordinal greater than a' ♯ b and a ♯ b' for a' < a and b' < b. The natural multiplication a ⨳ b is likewise recursively defined as the least ordinal such that a ⨳ b ♯ a' ⨳ b' is greater than a' ⨳ b ♯ a ⨳ b' for any a' < a and b' < b.

These operations form a rich algebraic structure: they're commutative, associative, preserve order, have the usual 0 and 1 from ordinals, and distribute over one another.

Moreover, these operations are the addition and multiplication of ordinals when viewed as combinatorial games. This makes them particularly useful for game theory.

Finally, both operations admit simple, intuitive descriptions in terms of the Cantor normal form. The natural addition of two ordinals corresponds to adding their Cantor normal forms as if they were polynomials in ω. Likewise, their natural multiplication corresponds to multiplying the Cantor normal forms as polynomials.

Implementation notes #

Given the rich algebraic structure of these two operations, we choose to create a type synonym nat_ordinal, where we provide the appropriate instances. However, to avoid casting back and forth between both types, we attempt to prove and state most results on ordinal.

Todo #

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

The identity function between nat_ordinal and ordinal.

Equations
@[protected]
noncomputable def nat_ordinal.rec {β : nat_ordinalSort u_2} (h : Π (a : ordinal), β (ordinal.to_nat_ordinal a)) (a : nat_ordinal) :
β a

A recursor for nat_ordinal. Use as induction x using nat_ordinal.rec.

Equations
theorem nat_ordinal.induction {p : nat_ordinal → Prop} (i : nat_ordinal) (h : ∀ (j : nat_ordinal), (∀ (k : nat_ordinal), k < jp k)p j) :
p i

ordinal.induction but for nat_ordinal.

noncomputable def ordinal.nadd  :

Natural addition on ordinals a ♯ b, also known as the Hessenberg sum, is recursively defined as the least ordinal greater than a' ♯ b and a ♯ b' for all a' < a and b' < b. In contrast to normal ordinal addition, it is commutative.

Natural addition can equivalently be characterized as the ordinal resulting from adding up corresponding coefficients in the Cantor normal forms of a and b.

Equations
theorem ordinal.nadd_def (a b : ordinal) :
a.nadd b = linear_order.max (a.blsub (λ (a' : ordinal) (h : a' < a), a'.nadd b)) (b.blsub (λ (b' : ordinal) (h : b' < b), a.nadd b'))
theorem ordinal.lt_nadd_iff {a b c : ordinal} :
a < b.nadd c (∃ (b' : ordinal) (H : b' < b), a b'.nadd c) ∃ (c' : ordinal) (H : c' < c), a b.nadd c'
theorem ordinal.nadd_le_iff {a b c : ordinal} :
b.nadd c a (∀ (b' : ordinal), b' < bb'.nadd c < a) ∀ (c' : ordinal), c' < cb.nadd c' < a
theorem ordinal.nadd_lt_nadd_left {b c : ordinal} (h : b < c) (a : ordinal) :
a.nadd b < a.nadd c
theorem ordinal.nadd_lt_nadd_right {b c : ordinal} (h : b < c) (a : ordinal) :
b.nadd a < c.nadd a
theorem ordinal.nadd_le_nadd_left {b c : ordinal} (h : b c) (a : ordinal) :
a.nadd b a.nadd c
theorem ordinal.nadd_le_nadd_right {b c : ordinal} (h : b c) (a : ordinal) :
b.nadd a c.nadd a
theorem ordinal.nadd_comm (a b : ordinal) :
a.nadd b = b.nadd a
theorem ordinal.blsub_nadd_of_mono (a b : ordinal) {f : Π (c : ordinal), c < a.nadd bordinal} (hf : ∀ {i j : ordinal} (hi : i < a.nadd b) (hj : j < a.nadd b), i jf i hi f j hj) :
(a.nadd b).blsub f = linear_order.max (a.blsub (λ (a' : ordinal) (ha' : a' < a), f (a'.nadd b) _)) (b.blsub (λ (b' : ordinal) (hb' : b' < b), f (a.nadd b') _))
theorem ordinal.nadd_assoc (a b c : ordinal) :
(a.nadd b).nadd c = a.nadd (b.nadd c)
@[simp]
theorem ordinal.nadd_zero (a : ordinal) :
a.nadd 0 = a
@[simp]
theorem ordinal.zero_nadd (a : ordinal) :
0.nadd a = a
@[simp]
theorem ordinal.nadd_one (a : ordinal) :
@[simp]
theorem ordinal.one_nadd (a : ordinal) :
theorem ordinal.nadd_succ (a b : ordinal) :
theorem ordinal.succ_nadd (a b : ordinal) :
@[simp]
theorem ordinal.nadd_nat (a : ordinal) (n : ) :
a.nadd n = a + n
@[simp]
theorem ordinal.nat_nadd (a : ordinal) (n : ) :
n.nadd a = a + n
theorem ordinal.add_le_nadd (a b : ordinal) :
a + b a.nadd b
@[protected, instance]
noncomputable def nat_ordinal.has_add  :
Equations
@[protected, instance]
Equations
@[simp]
theorem ordinal.lt_of_nadd_lt_nadd_left {a b c : ordinal} :
a.nadd b < a.nadd cb < c
theorem ordinal.lt_of_nadd_lt_nadd_right {a b c : ordinal} :
b.nadd a < c.nadd ab < c
theorem ordinal.le_of_nadd_le_nadd_left {a b c : ordinal} :
a.nadd b a.nadd cb c
theorem ordinal.le_of_nadd_le_nadd_right {a b c : ordinal} :
b.nadd a c.nadd ab c
theorem ordinal.nadd_lt_nadd_iff_left (a : ordinal) {b c : ordinal} :
a.nadd b < a.nadd c b < c
theorem ordinal.nadd_lt_nadd_iff_right (a : ordinal) {b c : ordinal} :
b.nadd a < c.nadd a b < c
theorem ordinal.nadd_le_nadd_iff_left (a : ordinal) {b c : ordinal} :
a.nadd b a.nadd c b c
theorem ordinal.nadd_le_nadd_iff_right (a : ordinal) {b c : ordinal} :
b.nadd a c.nadd a b c
theorem ordinal.nadd_left_cancel {a b c : ordinal} :
a.nadd b = a.nadd cb = c
theorem ordinal.nadd_right_cancel {a b c : ordinal} :
a.nadd b = c.nadd ba = c
theorem ordinal.nadd_left_cancel_iff {a b c : ordinal} :
a.nadd b = a.nadd c b = c
theorem ordinal.nadd_right_cancel_iff {a b c : ordinal} :
b.nadd a = c.nadd a b = c