Documentation

CombinatorialGames.Mathlib.NatOrdinal

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 NatOrdinal :

Type (u_1 + 1)

Equations

NatOrdinal = Ordinal.{?u.3}

Instances For

@[instance_reducible]

instance instNontrivialNatOrdinal :

Nontrivial NatOrdinal

Equations

instNontrivialNatOrdinal = Ordinal.nontrivial

@[instance_reducible]

instance instInhabitedNatOrdinal :

Inhabited NatOrdinal

Equations

instInhabitedNatOrdinal = Ordinal.inhabited

@[instance_reducible]

instance NatOrdinal.instPartialOrder :

PartialOrder NatOrdinal

Equations

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

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

Equations

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

NatOrdinal.type r < NatOrdinal.type s

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

C o

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

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

Equations

NatOrdinal.typein r = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => NatOrdinal.type (Subrel r fun (x : α) => r x a)) ⋯, top := NatOrdinal.type r, mem_range_iff_rel' := ⋯ }

Instances For

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

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

Equations

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

Instances For

@[simp]

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

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

theorem NatOrdinal.lt_wf :

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

instance NatOrdinal.instWellFoundedLT :

WellFoundedLT NatOrdinal

@[instance_reducible]

instance NatOrdinal.wellFoundedRelation :

WellFoundedRelation NatOrdinal

Equations

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

@[instance_reducible]

instance NatOrdinal.zero :

Zero NatOrdinal

Equations

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

@[instance_reducible]

instance NatOrdinal.one :

Equations

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

@[instance_reducible]

instance NatOrdinal.instOrderBot :

OrderBot NatOrdinal

Equations

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

instance NatOrdinal.instNoMaxOrder :

NoMaxOrder NatOrdinal

instance NatOrdinal.instZeroLEOneClass :

ZeroLEOneClass NatOrdinal

theorem 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) :

NatOrdinal.type r = NatOrdinal.type s

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

type r = 0

@[simp]

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

type r = 0 ↔ IsEmpty α

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

type r ≠ 0 ↔ Nonempty α

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

instance NatOrdinal.instNeZeroOfNat :

@[match_pattern]

def NatOrdinal.of :

Ordinal.{u_1} ≃o NatOrdinal

Equations

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

Instances For

@[match_pattern]

def NatOrdinal.val :

NatOrdinal ≃o Ordinal.{u_1}

Equations

NatOrdinal.val = OrderIso.refl NatOrdinal

Instances For

@[simp]

theorem NatOrdinal.of_symm :

@[simp]

theorem NatOrdinal.val_symm :

@[simp]

theorem NatOrdinal.of_val (a : NatOrdinal) :

of (val a) = a

@[simp]

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

val (of a) = a

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

val a ≤ b ↔ a ≤ of b

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

val a < b ↔ a < of b

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

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

of a < b ↔ a < val b

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

of a = b ↔ a = val b

@[simp]

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

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

@[simp]

theorem NatOrdinal.val_image_Iio (a : NatOrdinal) :

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

@[simp]

theorem NatOrdinal.bot_eq_zero :

@[simp]

theorem NatOrdinal.of_zero :

of 0 = 0

@[simp]

theorem NatOrdinal.val_zero :

val 0 = 0

@[simp]

theorem NatOrdinal.of_one :

of 1 = 1

@[simp]

theorem NatOrdinal.val_one :

val 1 = 1

@[simp]

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

of a = 0 ↔ a = 0

@[simp]

theorem NatOrdinal.val_eq_zero {a : NatOrdinal} :

val a = 0 ↔ a = 0

@[simp]

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

of a = 1 ↔ a = 1

@[simp]

theorem NatOrdinal.val_eq_one {a : NatOrdinal} :

val a = 1 ↔ a = 1

@[instance_reducible]

instance NatOrdinal.instSuccOrder :

SuccOrder NatOrdinal

Equations

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

theorem NatOrdinal.succ_def (a : NatOrdinal) :

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

@[simp]

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

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

@[simp]

theorem NatOrdinal.succ_ne_zero (a : NatOrdinal) :

Order.succ a ≠ 0

@[simp]

theorem NatOrdinal.succ_zero :

Order.succ 0 = 1

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

motive a

Equations

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

Instances For

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

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

@[simp]

theorem NatOrdinal.zero_le (a : NatOrdinal) :

0 ≤ a

@[simp]

theorem NatOrdinal.le_zero {a : NatOrdinal} :

a ≤ 0 ↔ a = 0

@[simp]

theorem NatOrdinal.not_lt_zero (a : NatOrdinal) :

¬a < 0

theorem NatOrdinal.pos_iff_ne_zero {a : NatOrdinal} :

0 < a ↔ a ≠ 0

theorem NatOrdinal.eq_zero_or_pos (a : NatOrdinal) :

a = 0 ∨ 0 < a

@[instance_reducible]

noncomputable instance NatOrdinal.instLinearOrder :

LinearOrder NatOrdinal

Equations

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

@[instance_reducible]

noncomputable instance NatOrdinal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NatOrdinal

Equations

NatOrdinal.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot NatOrdinal

instance NatOrdinal.instUncountable :

Uncountable NatOrdinal

@[simp]

theorem NatOrdinal.lt_one_iff_zero {a : NatOrdinal} :

a < 1 ↔ a = 0

@[simp]

theorem NatOrdinal.one_le_iff_ne_zero {a : NatOrdinal} :

1 ≤ a ↔ a ≠ 0

theorem NatOrdinal.le_one_iff {a : NatOrdinal} :

a ≤ 1 ↔ a = 0 ∨ a = 1

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

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

instance NatOrdinal.instSmallElemIio (a : NatOrdinal) :

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

instance NatOrdinal.instSmallElemIic (a : NatOrdinal) :

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

instance NatOrdinal.instSmallElemIco (a b : NatOrdinal) :

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

instance NatOrdinal.instSmallElemIcc (a b : NatOrdinal) :

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

instance NatOrdinal.instSmallElemIoo (a b : NatOrdinal) :

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

instance NatOrdinal.instSmallElemIoc (a b : NatOrdinal) :

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

instance NatOrdinal.instIsEmptyElemIioOfNat :

IsEmpty ↑(Set.Iio 0)

@[instance_reducible]

instance NatOrdinal.instUniqueElemIioOfNat :

Unique ↑(Set.Iio 1)

Equations

NatOrdinal.instUniqueElemIioOfNat = Ordinal.uniqueIioOne

@[simp]

theorem NatOrdinal.Iio_one_default_eq :

default = ⟨0, ⋯⟩

theorem NatOrdinal.bddAbove_iff_small {s : Set NatOrdinal} :

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

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

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

¬BddAbove sᶜ

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

f i ≤ iSup f

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

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

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.iSup_eq_zero_iff {ι : Type u_1} [Small.{u, u_1} ι] {f : ι → NatOrdinal} :

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

Natural addition #

@[instance_reducible]

instance 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

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_reducible]

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_reducible]

instance NatOrdinal.instSuccAddOrder :

SuccAddOrder NatOrdinal

Equations

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

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

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

theorem NatOrdinal.lt_omega0 {o : NatOrdinal} :

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

theorem NatOrdinal.nat_lt_omega0 (n : ℕ) :

↑n < of Ordinal.omega0

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

theorem NatOrdinal.lt_omega0' {o : NatOrdinal} :

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

theorem NatOrdinal.nat_lt_omega0' (n : ℕ) :

↑n < of Ordinal.omega0

@[simp]

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

a + b < c + a ↔ b < c

@[simp]

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

b + a < a + c ↔ b < c