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

Every real number has birthday at most ω. This can be proven by showing that a real number is equivalent to its Dedekind cut where only dyadic rationals are considered. At a later point, after we have the necessary API on dyadic numbers, we might want to prove this equivalence, or even re-define real numbers as Dedekind cuts of dyadic numbers specifically.

theorem Set.neg_image {α : Type u_1} {β : Type u_2} [InvolutiveNeg α] [InvolutiveNeg β] {s : Set β} {f : β → α} (h : ∀ x ∈ s, f (-x) = -f x) : -f '' s = f '' (-s)

ℝ to IGame

@[match_pattern]

def Real.toIGame (x : ℝ) : IGame

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

Equations

• ↑x = {Rat.cast '' {q : ℚ | ↑q < x} | Rat.cast '' {q : ℚ | 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 = Rat.cast '' {q : ℚ | ↑q < x}

@[simp]

theorem Real.rightMoves_toIGame (x : ℝ) : (↑x).rightMoves = Rat.cast '' {q : ℚ | x < ↑q}

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

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

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

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

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

theorem Real.mem_rightMoves_toIGame_of_lt {q : ℚ} {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_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_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_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 = {Rat.cast '' {q : ℚ | ↑q < x} | Rat.cast '' {q : ℚ | 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

theorem Real.toSurreal_def (x : ℝ) : ↑x = Surreal.ofSets (Rat.cast '' {q : ℚ | ↑q < x}) (Rat.cast '' {q : ℚ | 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_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Real.toSurreal_zero : ↑0 = 0

@[simp]

theorem Real.toSurreal_one : ↑1 = 1

@[simp]

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

@[simp]

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

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