Documentation

CombinatorialGames.NatOrdinal.Basic

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 give the ordinals a CommSemiring + IsStrictOrderedRing structure. To make the best use of it, we define them on a type alias NatOrdinal.

An equivalent characterization explains the relevance of these operations to game theory: they are the restrictions of surreal addition and multiplication to the ordinals.

Implementation notes #

To reduce API duplication, we opt not to implement operations on NatOrdinal on Ordinal. The order isomorphisms NatOrdinal.of and NatOrdinal.val allow us to cast between them whenever needed.

For similar reasons, most results about ordinals and games are written using NatOrdinal rather than Ordinal (except when Nimber would make more sense).

Basic casts between `Ordinal` and `NatOrdinal` #

theorem NatOrdinal.bddAbove_iff_small {s✝ : Set NatOrdinal} :

BddAbove s✝ ↔ Small.{u✝, u✝ + 1} ↑s✝

instance instZeroNatOrdinal :

Zero NatOrdinal

Equations

instZeroNatOrdinal = Ordinal.zero

theorem NatOrdinal.bddAbove_of_small (s✝ : Set NatOrdinal) [Small.{u✝, u✝ + 1} ↑s✝] :

@[simp]

theorem NatOrdinal.val_symm :

@[simp]

theorem NatOrdinal.of_image_Iio (a✝ : Ordinal.{u_1}) :

⇑of '' Set.Iio a✝ = Set.Iio (of a✝)

theorem NatOrdinal.not_bddAbove_compl_of_small (s✝ : Set NatOrdinal) [Small.{u✝, u✝ + 1} ↑s✝] :

¬BddAbove s✝ᶜ

@[simp]

theorem NatOrdinal.val_eq_zero {a✝ : NatOrdinal} :

val a✝ = 0 ↔ a✝ = 0

theorem NatOrdinal.succ_def (a✝ : NatOrdinal) :

Order.succ a✝ = of (val a✝ + 1)

theorem NatOrdinal.val_le_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ ≤ b✝ ↔ a✝ ≤ of b✝

@[simp]

theorem NatOrdinal.of_zero :

of 0 = 0

instance NatOrdinal.instSmallElemIoo (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ioo a✝ b✝)

instance NatOrdinal.instSuccOrder :

SuccOrder NatOrdinal

Equations

NatOrdinal.instSuccOrder = inferInstanceAs (SuccOrder Ordinal.{?u.2})

instance NatOrdinal.instSmallElemIio (a✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Iio a✝)

@[simp]

theorem NatOrdinal.of_val (a✝ : NatOrdinal) :

of (val a✝) = a✝

@[simp]

theorem NatOrdinal.Iio_one_default_eq :

default = ⟨0, ⋯⟩

instance instNontrivialNatOrdinal :

Nontrivial NatOrdinal

Equations

instNontrivialNatOrdinal = Ordinal.nontrivial

@[simp]

theorem NatOrdinal.val_of (a✝ : Ordinal.{u_1}) :

val (of a✝) = a✝

@[simp]

theorem NatOrdinal.of_eq_zero {a✝ : Ordinal.{u_1}} :

of a✝ = 0 ↔ a✝ = 0

noncomputable instance NatOrdinal.instLinearOrder :

LinearOrder NatOrdinal

Equations

NatOrdinal.instLinearOrder = Ordinal.instLinearOrder

@[match_pattern]

def NatOrdinal.val :

NatOrdinal ≃o Ordinal.{u_1}

The identity function between NatOrdinal and Ordinal._@.CombinatorialGames.NatOrdinal.Basic.3808482066._hygCtx._hyg.3.

Equations

NatOrdinal.val = OrderIso.refl NatOrdinal

Instances For

@[simp]

theorem NatOrdinal.bot_eq_zero :

theorem NatOrdinal.lt_wf :

WellFounded fun (x1 x2 : NatOrdinal) => x1 < x2

theorem NatOrdinal.iSup_le_iff {ι✝ : Type u_1} {f✝ : ι✝ → NatOrdinal} {a✝ : NatOrdinal} [Small.{u✝, u_1} ι✝] :

⨆ (i : ι✝), f✝ i ≤ a✝ ↔ ∀ (i : ι✝), f✝ i ≤ a✝

@[simp]

theorem NatOrdinal.succ_of (a✝ : Ordinal.{u_1}) :

Order.succ (of a✝) = of (a✝ + 1)

@[simp]

theorem NatOrdinal.of_symm :

theorem NatOrdinal.induction {p✝ : NatOrdinal → Prop} (i✝ : NatOrdinal) :

(∀ (j : NatOrdinal), (∀ k < j, p✝ k) → p✝ j) → p✝ i✝

Well-founded induction for NatOrdinal.

@[simp]

theorem NatOrdinal.one_le_iff_ne_zero {a✝ : NatOrdinal} :

1 ≤ a✝ ↔ a✝ ≠ 0

theorem NatOrdinal.iSup_eq_zero_iff {ι✝ : Type u_1} [Small.{u✝, u_1} ι✝] {f✝ : ι✝ → NatOrdinal} :

⨆ (i : ι✝), f✝ i = 0 ↔ ∀ (i : ι✝), f✝ i = 0

@[simp]

theorem NatOrdinal.of_eq_one {a✝ : Ordinal.{u_1}} :

of a✝ = 1 ↔ a✝ = 1

instance NatOrdinal.instUncountable :

Uncountable NatOrdinal

instance instOneNatOrdinal :

Equations

instOneNatOrdinal = Ordinal.one

instance NatOrdinal.instUniqueElemIioOfNat :

Unique ↑(Set.Iio 1)

Equations

NatOrdinal.instUniqueElemIioOfNat = Ordinal.uniqueIioOne

@[simp]

theorem NatOrdinal.val_eq_one {a✝ : NatOrdinal} :

val a✝ = 1 ↔ a✝ = 1

@[simp]

theorem NatOrdinal.val_image_Iio (a✝ : NatOrdinal) :

⇑val '' Set.Iio a✝ = Set.Iio (val a✝)

instance NatOrdinal.instPartialOrder :

PartialOrder NatOrdinal

Equations

NatOrdinal.instPartialOrder = inferInstanceAs (PartialOrder Ordinal.{?u.2})

@[simp]

theorem NatOrdinal.not_neg (a✝ : NatOrdinal) :

¬a✝ < 0

@[match_pattern]

def NatOrdinal.of :

Ordinal.{u_1} ≃o NatOrdinal

The identity function between Ordinal._@.CombinatorialGames.NatOrdinal.Basic.3808482066._hygCtx._hyg.3 and NatOrdinal.

Equations

NatOrdinal.of = OrderIso.refl Ordinal.{?u.2}

Instances For

theorem NatOrdinal.pos_iff_ne_zero {a✝ : NatOrdinal} :

0 < a✝ ↔ a✝ ≠ 0

instance NatOrdinal.instIsEmptyElemIioOfNat :

IsEmpty ↑(Set.Iio 0)

instance NatOrdinal.instSmallElemIoc (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ioc a✝ b✝)

@[simp]

theorem NatOrdinal.zero_le (a✝ : NatOrdinal) :

0 ≤ a✝

instance NatOrdinal.instSmallElemIcc (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Icc a✝ b✝)

instance NatOrdinal.instZeroLEOneClass :

ZeroLEOneClass NatOrdinal

instance NatOrdinal.instNoMaxOrder :

NoMaxOrder NatOrdinal

instance instInhabitedNatOrdinal :

Inhabited NatOrdinal

Equations

instInhabitedNatOrdinal = Ordinal.inhabited

@[simp]

theorem NatOrdinal.succ_zero :

Order.succ 0 = 1

theorem NatOrdinal.eq_natCast_of_le_natCast {a✝ : NatOrdinal} {b✝ : ℕ} :

a✝ ≤ of ↑b✝ → ∃ (c : ℕ), a✝ = of ↑c

instance NatOrdinal.instWellFoundedLT :

WellFoundedLT NatOrdinal

@[simp]

theorem NatOrdinal.succ_ne_zero (a✝ : NatOrdinal) :

Order.succ a✝ ≠ 0

theorem NatOrdinal.of_lt_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ < b✝ ↔ a✝ < val b✝

def NatOrdinal :

Type (u_1 + 1)

A type synonym for ordinals with natural addition and multiplication.

Equations

NatOrdinal = Ordinal.{?u.2}

Instances For

instance NatOrdinal.instSmallElemIco (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ico a✝ b✝)

instance NatOrdinal.instSmallElemIic (a✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Iic a✝)

@[simp]

theorem NatOrdinal.of_one :

of 1 = 1

theorem NatOrdinal.le_iSup {ι✝ : Type u_1} (f✝ : ι✝ → NatOrdinal) [Small.{u✝, u_1} ι✝] (i✝ : ι✝) :

f✝ i✝ ≤ iSup f✝

@[simp]

theorem NatOrdinal.val_one :

val 1 = 1

@[simp]

theorem NatOrdinal.le_zero {a✝ : NatOrdinal} :

a✝ ≤ 0 ↔ a✝ = 0

instance instWellFoundedRelationNatOrdinal :

WellFoundedRelation NatOrdinal

Equations

instWellFoundedRelationNatOrdinal = Ordinal.wellFoundedRelation

@[simp]

theorem NatOrdinal.val_zero :

val 0 = 0

instance NatOrdinal.instOrderBot :

OrderBot NatOrdinal

Equations

NatOrdinal.instOrderBot = inferInstanceAs (OrderBot Ordinal.{?u.2})

instance NatOrdinal.instNeZeroOfNat :

theorem NatOrdinal.val_eq_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ = b✝ ↔ a✝ = of b✝

theorem NatOrdinal.of_le_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ ≤ b✝ ↔ a✝ ≤ val b✝

noncomputable instance NatOrdinal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NatOrdinal

Equations

NatOrdinal.instConditionallyCompleteLinearOrderBot = inferInstanceAs (ConditionallyCompleteLinearOrderBot Ordinal.{?u.2})

@[simp]

theorem NatOrdinal.lt_one_iff_zero {a✝ : NatOrdinal} :

a✝ < 1 ↔ a✝ = 0

theorem NatOrdinal.lt_iSup_iff {ι✝ : Type u_1} [Small.{u✝, u_1} ι✝] (f✝ : ι✝ → NatOrdinal) {x✝ : NatOrdinal} :

x✝ < ⨆ (i : ι✝), f✝ i ↔ ∃ (i : ι✝), x✝ < f✝ i

theorem NatOrdinal.val_lt_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ < b✝ ↔ a✝ < of b✝

def NatOrdinal.ind {motive✝ : NatOrdinal → Sort u_1} (mk : (a : Ordinal.{u_2}) → motive✝ (of a)) (a✝ : NatOrdinal) :

motive✝ a✝

A recursor for NatOrdinal. Use as induction x.

Equations

NatOrdinal.ind mk a✝ = mk (NatOrdinal.val a✝)

Instances For

theorem NatOrdinal.eq_zero_or_pos (a✝ : NatOrdinal) :

a✝ = 0 ∨ 0 < a✝

theorem NatOrdinal.le_one_iff {a✝ : NatOrdinal} :

a✝ ≤ 1 ↔ a✝ = 0 ∨ a✝ = 1

theorem NatOrdinal.of_eq_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ = b✝ ↔ a✝ = val b✝

Natural addition #

@[irreducible]

noncomputable def NatOrdinal.add (a b : NatOrdinal) :

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

a.add b = max (⨆ (x : ↑(Set.Iio a)), Order.succ ((↑x).add b)) (⨆ (x : ↑(Set.Iio b)), Order.succ (a.add ↑x))

Instances For

instance NatOrdinal.instAdd :

Equations

NatOrdinal.instAdd = { add := NatOrdinal.add }

def NatOrdinal.«term_+ₒ_» :

Lean.TrailingParserDescr

Add two NatOrdinals as ordinal numbers.

Equations

NatOrdinal.«term_+ₒ_» = Lean.ParserDescr.trailingNode `NatOrdinal.«term_+ₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+ₒ") (Lean.ParserDescr.cat `term 66))

Instances For

theorem NatOrdinal.add_def (a b : NatOrdinal) :

a + b = max (⨆ (x : ↑(Set.Iio a)), Order.succ (↑x + b)) (⨆ (x : ↑(Set.Iio b)), Order.succ (a + ↑x))

theorem NatOrdinal.lt_add_iff {a b c : NatOrdinal} :

a < b + c ↔ (∃ b' < b, a ≤ b' + c) ∨ ∃ c' < c, a ≤ b + c'

theorem NatOrdinal.add_le_iff {a b c : NatOrdinal} :

b + c ≤ a ↔ (∀ b' < b, b' + c < a) ∧ ∀ c' < c, b + c' < a

instance NatOrdinal.instAddLeftStrictMono :

AddLeftStrictMono NatOrdinal

instance NatOrdinal.instAddRightStrictMono :

AddRightStrictMono NatOrdinal

instance NatOrdinal.instAddLeftMono :

AddLeftMono NatOrdinal

instance NatOrdinal.instAddRightMono :

AddRightMono NatOrdinal

instance NatOrdinal.instAddCommMonoid :

AddCommMonoid NatOrdinal

Equations

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

instance NatOrdinal.instIsOrderedCancelAddMonoid :

IsOrderedCancelAddMonoid NatOrdinal

theorem NatOrdinal.le_add_left {a b : NatOrdinal} :

a ≤ b + a

theorem NatOrdinal.le_add_right {a b : NatOrdinal} :

a ≤ a + b

@[simp]

theorem NatOrdinal.add_eq_zero_iff {a b : NatOrdinal} :

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

instance NatOrdinal.instSuccAddOrder :

SuccAddOrder NatOrdinal

Equations

NatOrdinal.instSuccAddOrder = { toSuccOrder := NatOrdinal.instSuccOrder, succ_eq_add_one := NatOrdinal.succ_eq_add_one'✝ }

@[simp]

theorem NatOrdinal.of_add_one (a : Ordinal.{u_1}) :

of (a + 1) = of a + 1

@[simp]

theorem NatOrdinal.val_add_one (a : NatOrdinal) :

val (a + 1) = val a + 1

@[simp]

theorem NatOrdinal.add_one_ne_zero (a : NatOrdinal) :

a + 1 ≠ 0

instance NatOrdinal.instAddMonoidWithOne :

AddMonoidWithOne NatOrdinal

Equations

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

@[simp]

theorem NatOrdinal.of_natCast (n : ℕ) :

of ↑n = ↑n

@[simp]

theorem NatOrdinal.val_natCast (n : ℕ) :

val ↑n = ↑n

@[simp]

theorem NatOrdinal.succ_one :

Order.succ 1 = 2

@[simp]

theorem NatOrdinal.natCast_image_Iio' (n : ℕ) :

Nat.cast '' Set.Iio n = Set.Iio ↑n

@[simp]

theorem NatOrdinal.natCast_image_Iio (n : ℕ) :

Nat.cast '' Set.Iio n = Set.Iio ↑n

@[simp]

theorem NatOrdinal.forall_lt_natCast {P : NatOrdinal → Prop} {n : ℕ} :

(∀ a < ↑n, P a) ↔ ∀ a < n, P ↑a

@[simp]

theorem NatOrdinal.exists_lt_natCast {P : NatOrdinal → Prop} {n : ℕ} :

(∃ a < ↑n, P a) ↔ ∃ a < n, P ↑a

instance NatOrdinal.instCharZero :

CharZero NatOrdinal

@[simp]

theorem NatOrdinal.of_add_natCast (a : Ordinal.{u_1}) (n : ℕ) :

of (a + ↑n) = of a + ↑n

@[simp]

theorem NatOrdinal.val_add_natCast (a : NatOrdinal) (n : ℕ) :

val (a + ↑n) = val a + ↑n

theorem NatOrdinal.oadd_le_add' (a b : Ordinal.{u_1}) :

a + b ≤ val (of a + of b)

A version of oadd_le_add stated in terms of Ordinal.

theorem NatOrdinal.oadd_le_add (a b : NatOrdinal) :

of (val a + val b) ≤ a + b

Natural multiplication #

@[irreducible]

noncomputable def NatOrdinal.mul (a b : NatOrdinal) :

Natural multiplication on ordinals a * b, also known as the Hessenberg product, is recursively defined as the least ordinal such that a * b + a' * b' is greater than a' * b + a * b' for all a' < a and b < b'. In contrast to normal ordinal multiplication, it is commutative and distributive (over natural addition).

Natural multiplication can equivalently be characterized as the ordinal resulting from multiplying the Cantor normal forms of a and b as if they were polynomials in ω. Addition of exponents is done via natural addition.

Equations

a.mul b = sInf {c : NatOrdinal | ∀ a' < a, ∀ b' < b, a'.mul b + a.mul b' < c + a'.mul b'}

Instances For

instance NatOrdinal.instMul :

Equations

NatOrdinal.instMul = { mul := NatOrdinal.mul }

def NatOrdinal.«term_*ₒ_» :

Lean.TrailingParserDescr

Multiply two NatOrdinals as ordinal numbers.

Equations

NatOrdinal.«term_*ₒ_» = Lean.ParserDescr.trailingNode `NatOrdinal.«term_*ₒ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*ₒ") (Lean.ParserDescr.cat `term 71))

Instances For

theorem NatOrdinal.mul_def (a b : NatOrdinal) :

a * b = sInf {c : NatOrdinal | ∀ a' < a, ∀ b' < b, a' * b + a * b' < c + a' * b'}

theorem NatOrdinal.mul_add_lt {a b a' b' : NatOrdinal} (ha : a' < a) (hb : b' < b) :

a' * b + a * b' < a * b + a' * b'

theorem NatOrdinal.mul_add_le {a b a' b' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) :

a' * b + a * b' ≤ a * b + a' * b'

theorem NatOrdinal.lt_mul_iff {a b c : NatOrdinal} :

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

theorem NatOrdinal.mul_le_iff {a b c : NatOrdinal} :

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

instance NatOrdinal.instCommMagma :

CommMagma NatOrdinal

Equations

NatOrdinal.instCommMagma = { toMul := NatOrdinal.instMul, mul_comm := NatOrdinal.mul_comm'✝ }

instance NatOrdinal.instMulZeroClass :

MulZeroClass NatOrdinal

Equations

NatOrdinal.instMulZeroClass = { toMul := NatOrdinal.instMul, toZero := instZeroNatOrdinal, zero_mul := NatOrdinal.instMulZeroClass._proof_1, mul_zero := NatOrdinal.mul_zero'✝ }

instance NatOrdinal.instMulZeroOneClass :

MulZeroOneClass NatOrdinal

Equations

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

instance NatOrdinal.instPosMulStrictMono :

PosMulStrictMono NatOrdinal

instance NatOrdinal.instMulPosStrictMono :

MulPosStrictMono NatOrdinal

instance NatOrdinal.instMulLeftMono :

MulLeftMono NatOrdinal

instance NatOrdinal.instMulRightMono :

MulRightMono NatOrdinal

instance NatOrdinal.instDistrib :

Distrib NatOrdinal

Equations

NatOrdinal.instDistrib = { toMul := NatOrdinal.instMul, toAdd := NatOrdinal.instAdd, left_distrib := NatOrdinal.mul_add✝, right_distrib := NatOrdinal.instDistrib._proof_1 }

theorem NatOrdinal.mul_add_lt₃ {a b c a' b' c' : NatOrdinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) :

a' * b * c + a * b' * c + a * b * c' + a' * b' * c' < a * b * c + a' * b' * c + a' * b * c' + a * b' * c'

theorem NatOrdinal.mul_add_le₃ {a b c a' b' c' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) :

a' * b * c + a * b' * c + a * b * c' + a' * b' * c' ≤ a * b * c + a' * b' * c + a' * b * c' + a * b' * c'

theorem NatOrdinal.lt_mul_iff₃ {a b c d : NatOrdinal} :

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

theorem NatOrdinal.mul_le_iff₃ {a b c d : NatOrdinal} :

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

instance NatOrdinal.instCommSemiring :

CommSemiring NatOrdinal

Equations

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

instance NatOrdinal.instIsStrictOrderedRing :

IsStrictOrderedRing NatOrdinal

theorem NatOrdinal.omul_le_mul' (a b : Ordinal.{u_1}) :

a * b ≤ val (of a * of b)

A version of omul_le_mul stated in terms of Ordinal.

theorem NatOrdinal.omul_le_mul (a b : NatOrdinal) :

of (val a * val b) ≤ a * b