Documentation

CombinatorialGames.Game.Small

Small games all around #

A small game is one that's smaller than all positive surreals, but larger than all negative surreals. The only small numeric games are zero, but surprisingly there are other non-numeric small games, such as the nimbers.

We prove that every dicotic game, and hence every impartial game is small. The former of these results is known as the lawnmower theorem.

source
class IGame.Small (x : IGame) :
Prop

Small games lie between all the positive and negative surreals.

  • lt_numeric_of_pos {y : IGame} [y.Numeric] : 0 < y → x < y

    A small game is smaller than any positive numeric game.

  • numeric_lt_of_neg {y : IGame} [y.Numeric] : y < 0 → y < x

    A small game is larger than any negative numeric game.

Instances
    source
    instance IGame.Small.zero :
    Small 0
    source
    theorem IGame.Small.lt_surreal_of_pos {x : IGame} [x.Small] {y : Surreal} (h : 0 < y) :
    Game.mk x < Surreal.toGame y
    source
    theorem IGame.Small.surreal_lt_of_neg {x : IGame} [x.Small] {y : Surreal} (h : y < 0) :
    Surreal.toGame y < Game.mk x
    source
    theorem IGame.Small.of_equiv {x y : IGame} (h : x ≈ y) [x.Small] :
    y.Small
    source
    theorem IGame.Small.congr {x y : IGame} (h : x ≈ y) :
    x.Small ↔ y.Small
    source
    theorem IGame.Numeric.small_iff_equiv_zero {x : IGame} [x.Numeric] :
    x.Small ↔ x ≈ 0
    source
    instance IGame.Small.neg (x : IGame) [x.Small] :
    (-x).Small
    source
    instance IGame.Small.add (x y : IGame) [x.Small] [y.Small] :
    (x + y).Small
    source
    instance IGame.Small.sub (x y : IGame) [x.Small] [y.Small] :
    (x - y).Small
    source
    instance IGame.Dicotic.toSmall (x : IGame) [x.Dicotic] :
    x.Small

    The lawnmower theorem: every dicotic game is small.

    source
    instance IGame.Impartial.toSmall (x : IGame) [x.Impartial] :
    x.Small