Small games all around

We define dicotic games, games x where both players can move from every nonempty subposition of x. We prove that these games are small, and relate them to infinitesimals.

TODO

• Define infinitesimal games as games x such that ∀ r : ℝ, 0 < r → -r < x ∧ x < r
  • (Does this hold for small infinitesimal games?)
• Prove that any short dicotic game is an infinitesimal (but not vice versa, consider ω⁻¹)

@[irreducible]

theorem IGame.Dicotic.lt_of_numeric_of_pos (x : IGame) [x.Dicotic] {y : IGame} [y.Numeric] (hy : 0 < y) : x < y

One half of the lawnmower theorem: any dicotic game is smaller than any positive numeric game.

theorem IGame.Dicotic.lt_of_numeric_of_neg (x : IGame) [x.Dicotic] {y : IGame} [y.Numeric] (hy : y < 0) : y < x

One half of the lawnmower theorem: any dicotic game is greater than any negative numeric game.

theorem IGame.Impartial.lt_of_numeric_of_pos (x : IGame) [x.Impartial] {y : IGame} [y.Numeric] (hy : 0 < y) : x < y

One half of the lawnmower theorem for impartial games.

theorem IGame.Impartial.lt_of_numeric_of_neg (x : IGame) [x.Impartial] {y : IGame} [y.Numeric] (hy : y < 0) : y < x

One half of the lawnmower theorem for impartial games.