Ordinals as games

We define the canonical map NatOrdinal → IGame, where every ordinal is mapped to the game whose left set consists of all previous ordinals. We make use of the type alias NatOrdinal rather than Ordinal, as this map also preserves addition, and in the case of surreals, multiplication. The map to surreals is defined in NatOrdinal.toSurreal.

We also prove some properties about NatCast, which is related to the previous construction by toIGame (↑n) ≈ ↑n.

Main declarations

• NatOrdinal.toIGame: The canonical map between NatOrdinal and IGame.
• NatOrdinal.toGame: The canonical map between NatOrdinal and Game.

Lemmas to upstream

@[simp]

theorem OrderEmbedding.antisymmRel_iff_antisymmRel {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) : f a ≈ f b ↔ a ≈ b

theorem OrderEmbedding.antisymmRel_iff_eq {α : Type u_1} {β : Type u_2} [Preorder α] [PartialOrder β] {a b : α} (f : α ↪o β) : f a ≈ f b ↔ a = b

theorem Ordinal.Iio_natCast (n : ℕ) : Set.Iio ↑n = Nat.cast '' Set.Iio n

theorem NatOrdinal.Iio_natCast (n : ℕ) : Set.Iio ↑n = Nat.cast '' 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.instSmallElemIio (o : NatOrdinal) : Small.{u, u + 1} ↑(Set.Iio o)

@[simp]

theorem NatOrdinal.zero_le (o : NatOrdinal) : 0 ≤ o

theorem NatOrdinal.not_lt_zero (o : NatOrdinal) : ¬o < 0

@[simp]

theorem NatOrdinal.lt_one_iff_zero {o : NatOrdinal} : o < 1 ↔ o = 0

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

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'

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.nmul_nadd_le {a b a' b' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) : a' * b + a * b' ≤ a * b + a' * b'

instance NatOrdinal.instCharZero : CharZero NatOrdinal

NatOrdinal to IGame

theorem NatOrdinal.toIGame'_def (o : NatOrdinal) : NatOrdinal.toIGame'✝ o = {NatOrdinal.toIGame'✝ '' Set.Iio o | ∅}ᴵ

def NatOrdinal.toIGame : NatOrdinal ↪o IGame

The canonical map from NatOrdinal to IGame, sending o to {Iio o | ∅}.

Equations

• NatOrdinal.toIGame = OrderEmbedding.ofStrictMono NatOrdinal.toIGame'✝ NatOrdinal.toIGame'_strictMono✝

theorem NatOrdinal.toIGame_def (o : NatOrdinal) : toIGame o = {⇑toIGame '' Set.Iio o | ∅}ᴵ

@[simp]

theorem NatOrdinal.leftMoves_toIGame (o : NatOrdinal) : (toIGame o).leftMoves = ⇑toIGame '' Set.Iio o

@[simp]

theorem NatOrdinal.rightMoves_toIGame (o : NatOrdinal) : (toIGame o).rightMoves = ∅

theorem NatOrdinal.forall_leftMoves_toIGame_natCast {P : IGame → Prop} {n : ℕ} : (∀ x ∈ (toIGame ↑n).leftMoves, P x) ↔ ∀ m < n, P (toIGame ↑m)

theorem NatOrdinal.exists_leftMoves_toIGame_natCast {P : IGame → Prop} {n : ℕ} : (∃ x ∈ (toIGame ↑n).leftMoves, P x) ↔ ∃ m < n, P (toIGame ↑m)

theorem NatOrdinal.forall_leftMoves_toIGame_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] : (∀ x ∈ (toIGame (OfNat.ofNat n)).leftMoves, P x) ↔ ∀ m < n, P (toIGame ↑m)

theorem NatOrdinal.exists_leftMoves_toIGame_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] : (∃ x ∈ (toIGame (OfNat.ofNat n)).leftMoves, P x) ↔ ∃ m < n, P (toIGame ↑m)

theorem NatOrdinal.mem_leftMoves_toIGame_of_lt {a b : NatOrdinal} (h : a < b) : toIGame a ∈ (toIGame b).leftMoves

@[simp]

theorem NatOrdinal.toIGame_zero : toIGame 0 = 0

@[simp]

theorem NatOrdinal.toIGame_one : toIGame 1 = 1

@[simp]

theorem NatOrdinal.not_toIGame_fuzzy (a b : NatOrdinal) : ¬toIGame a ‖ toIGame b

@[simp]

theorem NatOrdinal.toIGame_nonneg (a : NatOrdinal) : 0 ≤ toIGame a

NatOrdinal to Game

noncomputable def NatOrdinal.toGame : NatOrdinal ↪o Game

Converts an ordinal into the corresponding game.

Equations

• NatOrdinal.toGame = OrderEmbedding.ofStrictMono (fun (o : NatOrdinal) => Game.mk (NatOrdinal.toIGame o)) NatOrdinal.toGame._proof_1

@[simp]

theorem Game.mk_natOrdinal_toIGame (o : NatOrdinal) : mk (NatOrdinal.toIGame o) = NatOrdinal.toGame o

theorem NatOrdinal.toGame_def (o : NatOrdinal) : toGame o = {⇑toGame '' Set.Iio o | ∅}ᴳ

@[simp]

theorem NatOrdinal.toGame_zero : toGame 0 = 0

@[simp]

theorem NatOrdinal.toGame_one : toGame 1 = 1

@[simp]

theorem NatOrdinal.not_toGame_fuzzy (a b : NatOrdinal) : ¬toGame a ‖ toGame b

@[simp]

theorem NatOrdinal.toGame_nonneg (a : NatOrdinal) : 0 ≤ toGame a

@[irreducible]

theorem NatOrdinal.toIGame_add (a b : NatOrdinal) : toIGame (a + b) ≈ toIGame a + toIGame b

The natural addition of ordinals corresponds to their sum as games.

@[simp]

theorem NatOrdinal.toGame_add (a b : NatOrdinal) : toGame (a + b) = toGame a + toGame b

@[irreducible]

theorem NatOrdinal.toIGame_mul (a b : NatOrdinal) : toIGame (a * b) ≈ toIGame a * toIGame b

The natural multiplication of ordinals corresponds to their product as games.

@[simp]

theorem NatOrdinal.toGame_mul (a b : NatOrdinal) : toGame (a * b) = Game.mk (toIGame a * toIGame b)

def NatOrdinal.toGameAddHom : NatOrdinal →+o Game

NatOrdinal.toGame as an OrderAddMonoidHom.

Equations

• NatOrdinal.toGameAddHom = { toFun := ⇑NatOrdinal.toGame, map_zero' := NatOrdinal.toGame_zero, map_add' := NatOrdinal.toGame_add, monotone' := NatOrdinal.toGameAddHom._proof_1 }

@[simp]

theorem NatOrdinal.toGameAddHom_apply (a : NatOrdinal) : toGameAddHom a = toGame a

NatCast properties

@[simp]

theorem NatOrdinal.toGame_natCast (n : ℕ) : toGame ↑n = ↑n

theorem NatOrdinal.toIGame_natCast_equiv (n : ℕ) : toIGame ↑n ≈ ↑n

Note that the equality doesn't hold, as e.g. ↑2 = {1 | }, while toIGame 2 = {0, 1 | }.

@[irreducible]

theorem IGame.Short.exists_lt_natCast (x : IGame) [x.Short] : ∃ (n : ℕ), x < ↑n

theorem IGame.Short.exists_neg_natCast_lt (x : IGame) [x.Short] : ∃ (n : ℕ), -↑n < x

def IGame.termω : Lean.ParserDescr

Equations

• IGame.termω = Lean.ParserDescr.node `IGame.termω 1024 (Lean.ParserDescr.symbol "ω")

theorem IGame.Short.lt_omega0 (x : IGame) [x.Short] : x < NatOrdinal.toIGame (Ordinal.toNatOrdinal Ordinal.omega0)

theorem IGame.Short.neg_omega0_lt (x : IGame) [x.Short] : -NatOrdinal.toIGame (Ordinal.toNatOrdinal Ordinal.omega0) < x