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

noncomputable 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}}

@[implicit_reducible]

noncomputable instance Real.instCoeIGame : Coe ℝ IGame

Equations

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

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

@[simp]

theorem Real.leftMoves_toIGame (x : ℝ) : IGame.moves Player.left ↑x = Dyadic.toIGame '' {q : Dyadic | ↑↑q < x}

@[simp]

theorem Real.rightMoves_toIGame (x : ℝ) : IGame.moves Player.right ↑x = Dyadic.toIGame '' {q : Dyadic | x < ↑↑q}

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

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

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

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

theorem Real.mem_leftMoves_toIGame_of_lt {q : Dyadic} {x : ℝ} (h : ↑↑q < x) : ↑q ∈ IGame.moves Player.left ↑x

theorem Real.mem_rightMoves_toIGame_of_lt {q : Dyadic} {x : ℝ} (h : x < ↑↑q) : ↑q ∈ IGame.moves Player.right ↑x

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

noncomputable def Real.toGame (x : ℝ) : Game

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

Equations

• ↑x = Game.mk ↑x

@[implicit_reducible]

noncomputable 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 (q : Dyadic) => ↑↑q) '' {q : Dyadic | ↑↑q < x} | (fun (q : Dyadic) => ↑↑q) '' {q : Dyadic | x < ↑↑q}}

noncomputable 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

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

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

noncomputable def Real.toSurreal (x : ℝ) : Surreal

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

Equations

• ↑x = Surreal.mk ↑x

@[implicit_reducible]

noncomputable 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 = !{(fun (q : Dyadic) => ↑↑q) '' {q : Dyadic | ↑↑q < x} | (fun (q : Dyadic) => ↑↑q) '' {q : Dyadic | x < ↑↑q}}

noncomputable 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

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_eq_zero_iff {x : ℝ} : ↑x = 0 ↔ x = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

noncomputable 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