# mathlibdocumentation

set_theory.surreal

# Surreal numbers #

The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games.

A pregame is numeric if all the Left options are strictly smaller than all the Right options, and all those options are themselves numeric. In terms of combinatorial games, the numeric games have "frozen"; you can only make your position worse by playing, and Left is some definite "number" of moves ahead (or behind) Right.

A surreal number is an equivalence class of numeric pregames.

In fact, the surreals form a complete ordered field, containing a copy of the reals (and much else besides!) but we do not yet have a complete development.

## Order properties #

Surreal numbers inherit the relations ≤ and < from games, and these relations satisfy the axioms of a partial order (recall that x < y ↔ x ≤ y ∧ ¬ y ≤ x did not hold for games).

## Algebraic operations #

At this point, we have defined addition and negation (from pregames), and shown that surreals form an additive semigroup. It would be very little work to finish showing that the surreals form an ordered commutative group.

## Embeddings #

It would be nice projects to define the group homomorphism surreal → game, and also ℤ → surreal, and then the homomorphic inclusion of the dyadic rationals into surreals, and finally via dyadic Dedekind cuts the homomorphic inclusion of the reals into the surreals.

One can also map all the ordinals into the surreals!

## References #

def pgame.numeric  :
pgame → Prop

A pre-game is numeric if everything in the L set is less than everything in the R set, and all the elements of L and R are also numeric.

Equations
theorem pgame.numeric.move_left {x : pgame} (o : x.numeric) (i : x.left_moves) :
theorem pgame.numeric.move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
theorem pgame.numeric_rec {C : pgame → Prop} (H : ∀ (l r : Type u_1) (L : l → pgame) (R : r → pgame), (∀ (i : l) (j : r), L i < R j)(∀ (i : l), (L i).numeric)(∀ (i : r), (R i).numeric)(∀ (i : l), C (L i))(∀ (i : r), C (R i))C (pgame.mk l r L R)) (x : pgame) :
x.numericC x
theorem pgame.lt_asymm {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
x < y¬y < x
theorem pgame.le_of_lt {x y : pgame} (ox : x.numeric) (oy : y.numeric) (h : x < y) :
x y
theorem pgame.lt_iff_le_not_le {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
x < y x y ¬y x

On numeric pre-games, < and ≤ satisfy the axioms of a partial order (even though they don't on all pre-games).

theorem pgame.numeric_neg {x : pgame} (o : x.numeric) :
theorem pgame.numeric.move_left_lt {x : pgame} (o : x.numeric) (i : x.left_moves) :
x.move_left i < x
theorem pgame.numeric.move_left_le {x : pgame} (o : x.numeric) (i : x.left_moves) :
theorem pgame.numeric.lt_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
theorem pgame.numeric.le_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
theorem pgame.add_lt_add {w x y z : pgame} (ow : w.numeric) (ox : x.numeric) (oy : y.numeric) (oz : z.numeric) (hwx : w < x) (hyz : y < z) :
w + y < x + z
theorem pgame.numeric_add {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
(x + y).numeric
theorem pgame.numeric_nat (n : ) :

Pre-games defined by natural numbers are numeric.

The pre-game omega is numeric.

def surreal.equiv (x y : {x // x.numeric}) :
Prop

The equivalence on numeric pre-games.

Equations
@[instance]
def surreal.setoid  :
setoid {x // x.numeric}
Equations
def surreal  :
Type (u_1+1)

The type of surreal numbers. These are the numeric pre-games quotiented by the equivalence relation x ≈ y ↔ x ≤ y ∧ y ≤ x. In the quotient, the order becomes a total order.

Equations
def surreal.mk (x : pgame) (h : x.numeric) :

Construct a surreal number from a numeric pre-game.

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
def surreal.lift {α : Sort u_1} (f : Π (x : pgame), x.numeric → α) (H : ∀ {x y : pgame} (hx : x.numeric) (hy : y.numeric), x.equiv yf x hx = f y hy) :
surreal → α

Lift an equivalence-respecting function on pre-games to surreals.

Equations
def surreal.lift₂ {α : Sort u_1} (f : Π (x : pgame) (y : pgame), x.numericy.numeric → α) (H : ∀ {x₁ : pgame} {y₁ : pgame} {x₂ : pgame} {y₂ : pgame} (ox₁ : x₁.numeric) (oy₁ : y₁.numeric) (ox₂ : x₂.numeric) (oy₂ : y₂.numeric), x₁.equiv x₂y₁.equiv y₂f x₁ y₁ ox₁ oy₁ = f x₂ y₂ ox₂ oy₂) :
surrealsurreal → α

Lift a binary equivalence-respecting function on pre-games to surreals.

Equations
def surreal.le  :
surrealsurreal → Prop

The relation x ≤ y on surreals.

Equations
def surreal.lt  :
surrealsurreal → Prop

The relation x < y on surreals.

Equations
theorem surreal.not_le {x y : surreal} :
¬x.le y y.lt x

Addition on surreals is inherited from pre-game addition: the sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations
def surreal.neg  :

Negation for surreal numbers is inherited from pre-game negation: the negation of {L | R} is {-R | -L}.

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations