Documentation

LeanPool.MisereGames.Mathlib.NatOrdinal

Misere combinatorial games.

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

def MisereGames.NatOrdinal :

Type (u_1 + 1)

Ordinals equipped with natural arithmetic.

Equations

MisereGames.NatOrdinal = Ordinal.{?u.1}

Instances For

instance MisereGames.instNontrivialNatOrdinal :

Nontrivial NatOrdinal

@[implicit_reducible]

noncomputable instance MisereGames.instInhabitedNatOrdinal :

Inhabited NatOrdinal

Equations

MisereGames.instInhabitedNatOrdinal = { default := MisereGames.instInhabitedNatOrdinal._aux_1 }

@[implicit_reducible]

instance MisereGames.NatOrdinal.instPartialOrder :

PartialOrder NatOrdinal

Equations

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

def MisereGames.NatOrdinal.type {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] :

The natural ordinal represented by a well-order.

Equations

MisereGames.NatOrdinal.type r = ⟦{ α := α, r := r, wo := wo }⟧

Instances For

theorem PrincipalSeg.nat_ordinal_type_lt {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : PrincipalSeg r s) :

MisereGames.NatOrdinal.type r < MisereGames.NatOrdinal.type s

theorem MisereGames.NatOrdinal.inductionOn {C : NatOrdinal → Prop} (o : NatOrdinal) (H : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r], C (type r)) :

C o

def MisereGames.NatOrdinal.typein {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :

PrincipalSeg r fun (x1 x2 : NatOrdinal) => x1 < x2

The initial segment of NatOrdinal below the order type of r.

Equations

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

Instances For

noncomputable def MisereGames.NatOrdinal.enum {α : Type u} (r : α → α → Prop) [IsWellOrder α r] :

(fun (x1 x2 : ↑(Set.Iio (type r))) => x1 < x2) ≃r r

Enumerate the ordinals below a given order type by the original well-order.

Equations

MisereGames.NatOrdinal.enum r = (MisereGames.NatOrdinal.typein r).subrelIso

Instances For

@[simp]

theorem MisereGames.NatOrdinal.enum_symm_apply_coe {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a✝ : α) :

↑((enum r).symm a✝) = (typein r).toRelEmbedding a✝

theorem MisereGames.NatOrdinal.lt_wf :

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

instance MisereGames.NatOrdinal.instWellFoundedLT :

WellFoundedLT NatOrdinal

@[implicit_reducible]

instance MisereGames.NatOrdinal.wellFoundedRelation :

WellFoundedRelation NatOrdinal

Equations

MisereGames.NatOrdinal.wellFoundedRelation = { rel := fun (x1 x2 : MisereGames.NatOrdinal) => x1 < x2, wf := MisereGames.NatOrdinal.lt_wf }

@[implicit_reducible]

instance MisereGames.NatOrdinal.zero :

Zero NatOrdinal

Equations

MisereGames.NatOrdinal.zero = { zero := MisereGames.NatOrdinal.type emptyRelation }

@[implicit_reducible]

instance MisereGames.NatOrdinal.one :

Equations

MisereGames.NatOrdinal.one = { one := MisereGames.NatOrdinal.type emptyRelation }

@[implicit_reducible]

instance MisereGames.NatOrdinal.instOrderBot :

OrderBot NatOrdinal

Equations

MisereGames.NatOrdinal.instOrderBot = { bot := 0, bot_le := MisereGames.NatOrdinal.instOrderBot._proof_1 }

instance MisereGames.NatOrdinal.instNoMaxOrder :

NoMaxOrder NatOrdinal

instance MisereGames.NatOrdinal.instZeroLEOneClass :

ZeroLEOneClass NatOrdinal

theorem MisereGames.NatOrdinal.type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] :

type r = type s ↔ Nonempty (r ≃r s)

theorem RelIso.nat_ordinal_type_eq {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) :

MisereGames.NatOrdinal.type r = MisereGames.NatOrdinal.type s

theorem MisereGames.NatOrdinal.type_eq_zero_of_empty {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] [IsEmpty α] :

type r = 0

@[simp]

theorem MisereGames.NatOrdinal.type_eq_zero_iff_isEmpty {α : Type u} {r : α → α → Prop} [IsWellOrder α r] :

type r = 0 ↔ IsEmpty α

theorem MisereGames.NatOrdinal.type_ne_zero_iff_nonempty {α : Type u} {r : α → α → Prop} [IsWellOrder α r] :

type r ≠ 0 ↔ Nonempty α

theorem MisereGames.NatOrdinal.type_ne_zero_of_nonempty {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [h : Nonempty α] :

instance MisereGames.NatOrdinal.instNeZeroOfNat :

@[match_pattern]

def MisereGames.NatOrdinal.of :

Ordinal.{u_1} ≃o NatOrdinal

The order isomorphism from ordinals to NatOrdinal.

Equations

MisereGames.NatOrdinal.of = OrderIso.refl Ordinal.{?u.1}

Instances For

@[match_pattern]

def MisereGames.NatOrdinal.val :

NatOrdinal ≃o Ordinal.{u_1}

The order isomorphism from NatOrdinal to ordinals.

Equations

MisereGames.NatOrdinal.val = OrderIso.refl MisereGames.NatOrdinal

Instances For

@[simp]

theorem MisereGames.NatOrdinal.of_symm :

@[simp]

theorem MisereGames.NatOrdinal.val_symm :

@[simp]

theorem MisereGames.NatOrdinal.of_val (a : NatOrdinal) :

of (val a) = a

@[simp]

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

val (of a) = a

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

val a ≤ b ↔ a ≤ of b

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

val a < b ↔ a < of b

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

val a = b ↔ a = of b

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

of a ≤ b ↔ a ≤ val b

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

of a < b ↔ a < val b

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

of a = b ↔ a = val b

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

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

theorem MisereGames.NatOrdinal.val_image_Iio (a : NatOrdinal) :

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

@[simp]

theorem MisereGames.NatOrdinal.bot_eq_zero :

@[simp]

theorem MisereGames.NatOrdinal.of_zero :

of 0 = 0

@[simp]

theorem MisereGames.NatOrdinal.val_zero :

val 0 = 0

@[simp]

theorem MisereGames.NatOrdinal.of_one :

of 1 = 1

@[simp]

theorem MisereGames.NatOrdinal.val_one :

val 1 = 1

@[simp]

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

of a = 0 ↔ a = 0

@[simp]

theorem MisereGames.NatOrdinal.val_eq_zero {a : NatOrdinal} :

val a = 0 ↔ a = 0

@[simp]

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

of a = 1 ↔ a = 1

@[simp]

theorem MisereGames.NatOrdinal.val_eq_one {a : NatOrdinal} :

val a = 1 ↔ a = 1

@[implicit_reducible]

instance MisereGames.NatOrdinal.instSuccOrder :

SuccOrder NatOrdinal

Equations

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

theorem MisereGames.NatOrdinal.succ_def (a : NatOrdinal) :

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

@[simp]

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

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

theorem MisereGames.NatOrdinal.succ_ne_zero (a : NatOrdinal) :

Order.succ a ≠ 0

theorem MisereGames.NatOrdinal.succ_zero :

Order.succ 0 = 1

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

motive a

Recursor through the underlying ordinal representation.

Equations

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

Instances For

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

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

@[simp]

theorem MisereGames.NatOrdinal.zero_le (a : NatOrdinal) :

0 ≤ a

@[simp]

theorem MisereGames.NatOrdinal.le_zero {a : NatOrdinal} :

a ≤ 0 ↔ a = 0

@[simp]

theorem MisereGames.NatOrdinal.not_lt_zero (a : NatOrdinal) :

¬a < 0

theorem MisereGames.NatOrdinal.pos_iff_ne_zero {a : NatOrdinal} :

0 < a ↔ a ≠ 0

theorem MisereGames.NatOrdinal.eq_zero_or_pos (a : NatOrdinal) :

a = 0 ∨ 0 < a

@[implicit_reducible]

noncomputable instance MisereGames.NatOrdinal.instLinearOrder :

LinearOrder NatOrdinal

Equations

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

@[implicit_reducible]

noncomputable instance MisereGames.NatOrdinal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NatOrdinal

Equations

MisereGames.NatOrdinal.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot MisereGames.NatOrdinal

instance MisereGames.NatOrdinal.instUncountable :

Uncountable NatOrdinal

@[simp]

theorem MisereGames.NatOrdinal.lt_one_iff_zero {a : NatOrdinal} :

a < 1 ↔ a = 0

@[simp]

theorem MisereGames.NatOrdinal.one_le_iff_ne_zero {a : NatOrdinal} :

1 ≤ a ↔ a ≠ 0

theorem MisereGames.NatOrdinal.le_one_iff {a : NatOrdinal} :

a ≤ 1 ↔ a = 0 ∨ a = 1

theorem MisereGames.NatOrdinal.eq_natCast_of_le_natCast {a : NatOrdinal} {b : ℕ} (h : a ≤ of ↑b) :

∃ (c : ℕ), a = of ↑c

instance MisereGames.NatOrdinal.instSmallElemIio (a : NatOrdinal) :

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

instance MisereGames.NatOrdinal.instSmallElemIic (a : NatOrdinal) :

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

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

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

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

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

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

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

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

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

instance MisereGames.NatOrdinal.instIsEmptyElemIioOfNat :

IsEmpty ↑(Set.Iio 0)

@[implicit_reducible]

instance MisereGames.NatOrdinal.instUniqueElemIioOfNat :

Unique ↑(Set.Iio 1)

Equations

MisereGames.NatOrdinal.instUniqueElemIioOfNat = Ordinal.uniqueIioOne

@[simp]

theorem MisereGames.NatOrdinal.Iio_one_default_eq :

default = ⟨0, ⋯⟩

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

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

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

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

¬BddAbove sᶜ

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

f i ≤ iSup f

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

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

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

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

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

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

Natural addition #

@[implicit_reducible]

noncomputable instance MisereGames.NatOrdinal.instAdd :

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

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

def MisereGames.NatOrdinal.«term_+ₒ_» :

Lean.TrailingParserDescr

Add two NatOrdinals as ordinal numbers.

Equations

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

Instances For

theorem MisereGames.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 MisereGames.NatOrdinal.lt_add_iff {a b c : NatOrdinal} :

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

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

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

instance MisereGames.NatOrdinal.instAddLeftStrictMono :

AddLeftStrictMono NatOrdinal

instance MisereGames.NatOrdinal.instAddRightStrictMono :

AddRightStrictMono NatOrdinal

instance MisereGames.NatOrdinal.instAddLeftMono :

AddLeftMono NatOrdinal

instance MisereGames.NatOrdinal.instAddRightMono :

AddRightMono NatOrdinal

@[implicit_reducible]

noncomputable instance MisereGames.NatOrdinal.instAddCommMonoid :

AddCommMonoid NatOrdinal

Equations

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

instance MisereGames.NatOrdinal.instIsOrderedCancelAddMonoid :

IsOrderedCancelAddMonoid NatOrdinal

theorem MisereGames.NatOrdinal.le_add_left {a b : NatOrdinal} :

a ≤ b + a

theorem MisereGames.NatOrdinal.le_add_right {a b : NatOrdinal} :

a ≤ a + b

@[simp]

theorem MisereGames.NatOrdinal.add_eq_zero_iff {a b : NatOrdinal} :

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

@[implicit_reducible]

instance MisereGames.NatOrdinal.instSuccAddOrder :

SuccAddOrder NatOrdinal

Equations

MisereGames.NatOrdinal.instSuccAddOrder = { toSuccOrder := MisereGames.NatOrdinal.instSuccOrder, succ_eq_add_one := MisereGames.NatOrdinal.instSuccAddOrder._proof_1 }

@[simp]

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

of (a + 1) = of a + 1

@[simp]

theorem MisereGames.NatOrdinal.val_add_one (a : NatOrdinal) :

val (a + 1) = val a + 1

theorem MisereGames.NatOrdinal.add_one_ne_zero (a : NatOrdinal) :

a + 1 ≠ 0

@[implicit_reducible]

noncomputable instance MisereGames.NatOrdinal.instAddMonoidWithOne :

AddMonoidWithOne NatOrdinal

Equations

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

@[simp]

theorem MisereGames.NatOrdinal.of_natCast (n : ℕ) :

of ↑n = ↑n

@[simp]

theorem MisereGames.NatOrdinal.val_natCast (n : ℕ) :

val ↑n = ↑n

theorem MisereGames.NatOrdinal.succ_one :

Order.succ 1 = 2

theorem MisereGames.NatOrdinal.natCast_image_Iio' (n : ℕ) :

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

@[simp]

theorem MisereGames.NatOrdinal.natCast_image_Iio (n : ℕ) :

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

@[simp]

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

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

@[simp]

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

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

theorem MisereGames.NatOrdinal.lt_omega0 {o : NatOrdinal} :

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

theorem MisereGames.NatOrdinal.nat_lt_omega0 (n : ℕ) :

↑n < of Ordinal.omega0

instance MisereGames.NatOrdinal.instCharZero :

CharZero NatOrdinal

@[simp]

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

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

@[simp]

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

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

theorem MisereGames.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 MisereGames.NatOrdinal.oadd_le_add (a b : NatOrdinal) :

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

theorem MisereGames.NatOrdinal.lt_omega0' {o : NatOrdinal} :

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

theorem MisereGames.NatOrdinal.nat_lt_omega0' (n : ℕ) :

↑n < of Ordinal.omega0

@[simp]

theorem MisereGames.NatOrdinal.add_lt_add_iff_left_right {a b c : NatOrdinal} :

a + b < c + a ↔ b < c

@[simp]

theorem MisereGames.NatOrdinal.add_lt_add_iff_right_left {a b c : NatOrdinal} :

b + a < a + c ↔ b < c