Real numbers as games

We define the function Real.toIGame, casting a real number to its Dedekind cut, and prove that it's an order embedding. We then define the Game and Surreal versions of this map, and prove that they are ring and field homomorphisms respectively.

TODO

Prove that every real number has birthday at most ω.

theorem exists_div_btwn {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} {n : ℕ} (h : x < y) (nh : (y - x)⁻¹ < ↑n) : ∃ (z : ℤ), x < ↑z / ↑n ∧ ↑z / ↑n < y

theorem exists_dyadic_btwn {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : x < y) : ∃ (q : Dyadic), x < ↑↑q ∧ ↑↑q < y

ℝ to IGame

@[match_pattern]

def Real.toIGame (x : ℝ) : IGame

The canonical map from ℝ to IGame, sending a real number to its Dedekind cut of dyadic rationals.

Equations

• ↑x = {Dyadic.toIGame '' {q : Dyadic | ↑↑q < x} | Dyadic.toIGame '' {q : Dyadic | x < ↑↑q}}ᴵ

instance Real.instCoeIGame : Coe ℝ IGame

Equations

• Real.instCoeIGame = { coe := Real.toIGame }

instance Real.Numeric.toIGame (x : ℝ) : (↑x).Numeric

@[simp]

theorem Real.leftMoves_toIGame (x : ℝ) : (↑x).leftMoves = Dyadic.toIGame '' {q : Dyadic | ↑↑q < x}

@[simp]

theorem Real.rightMoves_toIGame (x : ℝ) : (↑x).rightMoves = Dyadic.toIGame '' {q : Dyadic | x < ↑↑q}

theorem Real.forall_leftMoves_toIGame {P : IGame → Prop} {x : ℝ} : (∀ y ∈ (↑x).leftMoves, P y) ↔ ∀ (q : Dyadic), ↑↑q < x → P ↑q

theorem Real.exists_leftMoves_toIGame {P : IGame → Prop} {x : ℝ} : (∃ y ∈ (↑x).leftMoves, P y) ↔ ∃ (q : Dyadic), ↑↑q < x ∧ P ↑q

theorem Real.forall_rightMoves_toIGame {P : IGame → Prop} {x : ℝ} : (∀ y ∈ (↑x).rightMoves, P y) ↔ ∀ (q : Dyadic), x < ↑↑q → P ↑q

theorem Real.exists_rightMoves_toIGame {P : IGame → Prop} {x : ℝ} : (∃ y ∈ (↑x).rightMoves, P y) ↔ ∃ (q : Dyadic), x < ↑↑q ∧ P ↑q

theorem Real.mem_leftMoves_toIGame_of_lt {q : Dyadic} {x : ℝ} (h : ↑↑q < x) : ↑q ∈ (↑x).leftMoves

theorem Real.mem_rightMoves_toIGame_of_lt {q : Dyadic} {x : ℝ} (h : x < ↑↑q) : ↑q ∈ (↑x).rightMoves

def Real.toIGameEmbedding : ℝ ↪o IGame

Real.toIGame as an OrderEmbedding.

Equations

• Real.toIGameEmbedding = OrderEmbedding.ofStrictMono Real.toIGame Real.toIGameEmbedding._proof_1

@[simp]

theorem Real.toIGameEmbedding_apply (x : ℝ) : toIGameEmbedding x = ↑x

@[simp]

theorem Real.toIGame_le_iff {x y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Real.toIGame_lt_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem Real.toIGame_equiv_iff {x y : ℝ} : ↑x ≈ ↑y ↔ x = y

@[simp]

theorem Real.toIGame_inj {x y : ℝ} : ↑x = ↑y ↔ x = y

@[simp]

theorem Real.toIGame_neg (x : ℝ) : ↑(-x) = -↑x

theorem Real.toIGame_ratCast_equiv (q : ℚ) : ↑↑q ≈ ↑q

theorem Real.toIGame_dyadic_equiv (q : Dyadic) : ↑↑↑q ≈ ↑q

theorem Real.toIGame_natCast_equiv (n : ℕ) : ↑↑n ≈ ↑n

theorem Real.toIGame_intCast_equiv (n : ℤ) : ↑↑n ≈ ↑n

theorem Real.toIGame_zero_equiv : ↑0 ≈ 0

theorem Real.toIGame_one_equiv : ↑1 ≈ 1

@[simp]

theorem Real.ratCast_lt_toIGame {q : ℚ} {x : ℝ} : ↑q < ↑x ↔ ↑q < x

@[simp]

theorem Real.toIGame_lt_ratCast {q : ℚ} {x : ℝ} : ↑x < ↑q ↔ x < ↑q

@[simp]

theorem Real.ratCast_le_toIGame {q : ℚ} {x : ℝ} : ↑q ≤ ↑x ↔ ↑q ≤ x

@[simp]

theorem Real.toIGame_le_ratCast {q : ℚ} {x : ℝ} : ↑x ≤ ↑q ↔ x ≤ ↑q

@[simp]

theorem Real.ratCast_equiv_toIGame {q : ℚ} {x : ℝ} : ↑q ≈ ↑x ↔ ↑q = x

@[simp]

theorem Real.toIGame_equiv_ratCast {q : ℚ} {x : ℝ} : ↑x ≈ ↑q ↔ x = ↑q

theorem Real.toIGame_add_ratCast_equiv (x : ℝ) (q : ℚ) : ↑(x + ↑q) ≈ ↑x + ↑q

theorem Real.toIGame_ratCast_add_equiv (q : ℚ) (x : ℝ) : ↑(↑q + x) ≈ ↑q + ↑x

theorem Real.toIGame_add_dyadic_equiv (x : ℝ) (q : Dyadic) : ↑(x + ↑↑q) ≈ ↑x + ↑q

theorem Real.toIGame_dyadic_add_equiv (q : Dyadic) (x : ℝ) : ↑(↑↑q + x) ≈ ↑q + ↑x

theorem Real.toIGame_add_equiv (x y : ℝ) : ↑(x + y) ≈ ↑x + ↑y

theorem Real.toIGame_sub_ratCast_equiv (x : ℝ) (q : ℚ) : ↑(x - ↑q) ≈ ↑x - ↑q

theorem Real.toIGame_ratCast_sub_equiv (q : ℚ) (x : ℝ) : ↑(↑q - x) ≈ ↑q - ↑x

theorem Real.toIGame_sub_dyadic_equiv (x : ℝ) (q : Dyadic) : ↑(x - ↑↑q) ≈ ↑x - ↑q

theorem Real.toIGame_dyadic_sub_equiv (q : Dyadic) (x : ℝ) : ↑(↑↑q - x) ≈ ↑q - ↑x

theorem Real.toIGame_sub_equiv (x y : ℝ) : ↑(x - y) ≈ ↑x - ↑y

ℝ to Game

@[match_pattern]

def Real.toGame (x : ℝ) : Game

The canonical map from ℝ to Game, sending a real number to its Dedekind cut.

Equations

• ↑x = Game.mk ↑x

instance Real.instCoeGame : Coe ℝ Game

Equations

• Real.instCoeGame = { coe := Real.toGame }

@[simp]

theorem Game.mk_real_toIGame (x : ℝ) : mk ↑x = ↑x

theorem Real.toGame_def (x : ℝ) : ↑x = {(fun (x : Dyadic) => ↑↑x) '' {q : Dyadic | ↑↑q < x} | (fun (x : Dyadic) => ↑↑x) '' {q : Dyadic | x < ↑↑q}}ᴳ

def Real.toGameEmbedding : ℝ ↪o Game

Real.toGame as an OrderEmbedding.

Equations

• Real.toGameEmbedding = OrderEmbedding.ofStrictMono Real.toGame ⋯

@[simp]

theorem Real.toGameEmbedding_apply (x : ℝ) : toGameEmbedding x = ↑x

@[simp]

theorem Real.toGame_le_iff {x y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Real.toGame_lt_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem Real.toGame_equiv_iff {x y : ℝ} : ↑x ≈ ↑y ↔ x = y

@[simp]

theorem Real.toGame_inj {x y : ℝ} : ↑x = ↑y ↔ x = y

@[simp]

theorem Real.toGame_ratCast (q : ℚ) : ↑↑q = ↑q

@[simp]

theorem Real.toGame_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Real.toGame_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Real.toGame_zero : ↑0 = 0

@[simp]

theorem Real.toGame_one : ↑1 = 1

@[simp]

theorem Real.toGame_add (x y : ℝ) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Real.toGame_sub (x y : ℝ) : ↑(x - y) = ↑x - ↑y

def Real.toGameAddHom : ℝ →+o Game

Real.toGame as an OrderAddMonoidHom.

Equations

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

@[simp]

theorem Real.toGameAddHom_apply (x : ℝ) : toGameAddHom x = ↑x

ℝ to Surreal

@[match_pattern]

def Real.toSurreal (x : ℝ) : Surreal

The canonical map from ℝ to Surreal, sending a real number to its Dedekind cut.

Equations

• ↑x = Surreal.mk ↑x

instance Real.instCoeSurreal : Coe ℝ Surreal

Equations

• Real.instCoeSurreal = { coe := Real.toSurreal }

@[simp]

theorem Surreal.mk_real_toIGame (x : ℝ) : mk ↑x = ↑x

@[simp]

theorem Real.toGame_toSurreal (x : ℝ) : Surreal.toGame ↑x = ↑x

theorem Real.toSurreal_def (x : ℝ) : ↑x = Surreal.ofSets ((fun (x : Dyadic) => ↑↑x) '' {q : Dyadic | ↑↑q < x}) ((fun (x : Dyadic) => ↑↑x) '' {q : Dyadic | x < ↑↑q}) ⋯

def Real.toSurrealEmbedding : ℝ ↪o Surreal

Real.toSurreal as an OrderEmbedding.

Equations

• Real.toSurrealEmbedding = OrderEmbedding.ofStrictMono Real.toSurreal ⋯

@[simp]

theorem Real.toSurrealEmbedding_apply (x : ℝ) : toSurrealEmbedding x = ↑x

@[simp]

theorem Real.toSurreal_le_iff {x y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Real.toSurreal_lt_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem Real.toSurreal_equiv_iff {x y : ℝ} : ↑x ≈ ↑y ↔ x = y

@[simp]

theorem Real.toSurreal_inj {x y : ℝ} : ↑x = ↑y ↔ x = y

@[simp]

theorem Real.toSurreal_ratCast (q : ℚ) : ↑↑q = ↑q

@[simp]

theorem Real.toSurreal_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Real.toSurreal_ofNat (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = ↑n

@[simp]

theorem Real.toSurreal_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Real.toSurreal_zero : ↑0 = 0

@[simp]

theorem Real.toSurreal_one : ↑1 = 1

@[simp]

theorem Real.toSurreal_neg (x : ℝ) : ↑(-x) = -↑x

@[simp]

theorem Real.toSurreal_add (x y : ℝ) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Real.toSurreal_sub (x y : ℝ) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Real.toSurreal_max (x y : ℝ) : ↑(max x y) = max ↑x ↑y

@[simp]

theorem Real.toSurreal_min (x y : ℝ) : ↑(min x y) = min ↑x ↑y

@[simp]

theorem Real.toSurreal_abs (x : ℝ) : ↑|x| = |↑x|

For convenience, we deal with multiplication after defining Real.toSurreal.

theorem Real.toIGame_mul_ratCast_equiv (x : ℝ) (q : ℚ) : ↑(x * ↑q) ≈ ↑x * ↑q

theorem Real.toIGame_ratCast_mul_equiv (q : ℚ) (x : ℝ) : ↑(↑q * x) ≈ ↑q * ↑x

theorem Real.toIGame_mul_equiv (x y : ℝ) : ↑(x * y) ≈ ↑x * ↑y

@[simp]

theorem Real.toSurreal_mul (x y : ℝ) : ↑(x * y) = ↑x * ↑y

def Real.toSurrealRingHom : ℝ →+*o Surreal

Real.toSurreal as an OrderRingHom.

Equations

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

@[simp]

theorem Real.toSurrealRingHom_toFun (x : ℝ) : toSurrealRingHom x = ↑x

@[simp]

theorem Real.toSurreal_inv (x : ℝ) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem Real.toSurreal_div (x y : ℝ) : ↑(x / y) = ↑x / ↑y

theorem Real.toIGame_inv_equiv (x : ℝ) : ↑x⁻¹ ≈ (↑x)⁻¹

theorem Real.toIGame_div_equiv (x y : ℝ) : ↑(x / y) ≈ ↑x / ↑y

Simp lemmas

Dyadic

@[simp]

theorem Real.dyadic_lt_toIGame {q : Dyadic} {x : ℝ} : ↑q < ↑x ↔ ↑↑q < x

@[simp]

theorem Real.toIGame_lt_dyadic {q : Dyadic} {x : ℝ} : ↑x < ↑q ↔ x < ↑↑q

@[simp]

theorem Real.dyadic_le_toIGame {q : Dyadic} {x : ℝ} : ↑q ≤ ↑x ↔ ↑↑q ≤ x

@[simp]

theorem Real.toIGame_le_dyadic {q : Dyadic} {x : ℝ} : ↑x ≤ ↑q ↔ x ≤ ↑↑q

@[simp]

theorem Real.dyadic_equiv_toIGame {q : Dyadic} {x : ℝ} : ↑q ≈ ↑x ↔ ↑↑q = x

@[simp]

theorem Real.toIGame_equiv_dyadic {q : Dyadic} {x : ℝ} : ↑x ≈ ↑q ↔ x = ↑↑q

ℤ

@[simp]

theorem Real.toIGame_lt_intCast {x : ℝ} {y : ℤ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Real.toIGame_le_intCast {x : ℝ} {y : ℤ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Real.intCast_lt_toIGame {x : ℤ} {y : ℝ} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Real.intCast_le_toIGame {x : ℤ} {y : ℝ} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Real.toIGame_equiv_intCast {x : ℝ} {y : ℤ} : ↑x ≈ ↑y ↔ x = ↑y

@[simp]

theorem Real.intCast_equiv_toIGame {x : ℤ} {y : ℝ} : ↑x ≈ ↑y ↔ ↑x = y

ℕ

@[simp]

theorem Real.toIGame_lt_natCast {x : ℝ} {y : ℕ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Real.toIGame_le_natCast {x : ℝ} {y : ℕ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Real.natCast_lt_toIGame {x : ℕ} {y : ℝ} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Real.natCast_le_toIGame {x : ℕ} {y : ℝ} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Real.toIGame_equiv_natCast {x : ℝ} {y : ℕ} : ↑x ≈ ↑y ↔ x = ↑y

@[simp]

theorem Real.natCast_equiv_toIGame {x : ℕ} {y : ℝ} : ↑x ≈ ↑y ↔ ↑x = y

0

@[simp]

theorem Real.toIGame_lt_zero {x : ℝ} : ↑x < 0 ↔ x < 0

@[simp]

theorem Real.toIGame_le_zero {x : ℝ} : ↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem Real.zero_lt_toIGame {x : ℝ} : 0 < ↑x ↔ 0 < x

@[simp]

theorem Real.zero_le_toIGame {x : ℝ} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Real.toIGame_equiv_zero {x : ℝ} : ↑x ≈ 0 ↔ x = 0

@[simp]

theorem Real.zero_equiv_toIGame {x : ℝ} : 0 ≈ ↑x ↔ 0 = x

1

@[simp]

theorem Real.toIGame_lt_one {x : ℝ} : ↑x < 1 ↔ x < 1

@[simp]

theorem Real.toIGame_le_one {x : ℝ} : ↑x ≤ 1 ↔ x ≤ 1

@[simp]

theorem Real.one_lt_toIGame {x : ℝ} : 1 < ↑x ↔ 1 < x

@[simp]

theorem Real.one_le_toIGame {x : ℝ} : 1 ≤ ↑x ↔ 1 ≤ x

@[simp]

theorem Real.toIGame_equiv_one {x : ℝ} : ↑x ≈ 1 ↔ x = 1

@[simp]

theorem Real.one_equiv_toIGame {x : ℝ} : 1 ≈ ↑x ↔ 1 = x