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 ω⁻¹)

Dicotic games

class IGame.Dicotic (x : IGame) : Prop

A game x is dicotic if both players can move from every nonempty subposition of x.

• out : IGame.DicoticAux✝ x

theorem IGame.dicotic_iff_aux (x : IGame) : x.Dicotic ↔ IGame.DicoticAux✝ x

theorem IGame.dicotic_def {x : IGame} : x.Dicotic ↔ (x.leftMoves = ∅ ↔ x.rightMoves = ∅) ∧ (∀ l ∈ x.leftMoves, l.Dicotic) ∧ ∀ r ∈ x.rightMoves, r.Dicotic

theorem IGame.Dicotic.eq_zero_iff {x : IGame} [hx : x.Dicotic] : x = 0 ↔ x.leftMoves = ∅ ∨ x.rightMoves = ∅

theorem IGame.Dicotic.ne_zero_iff {x : IGame} [x.Dicotic] : x ≠ 0 ↔ x.leftMoves ≠ ∅ ∧ x.rightMoves ≠ ∅

theorem IGame.Dicotic.mk' {x : IGame} (h : x.leftMoves = ∅ ↔ x.rightMoves = ∅) (hl : ∀ y ∈ x.leftMoves, y.Dicotic) (hr : ∀ y ∈ x.rightMoves, y.Dicotic) : x.Dicotic

theorem IGame.Dicotic.leftMoves_eq_empty_iff {x : IGame} [hx : x.Dicotic] : x.leftMoves = ∅ ↔ x.rightMoves = ∅

theorem IGame.Dicotic.rightMoves_eq_empty_iff {x : IGame} [hx : x.Dicotic] : x.rightMoves = ∅ ↔ x.leftMoves = ∅

theorem IGame.Dicotic.of_mem_leftMoves {x y : IGame} [hx : x.Dicotic] (h : y ∈ x.leftMoves) : y.Dicotic

theorem IGame.Dicotic.of_mem_rightMoves {x y : IGame} [hx : x.Dicotic] (h : y ∈ x.rightMoves) : y.Dicotic

@[simp]

instance IGame.Dicotic.zero : Dicotic 0

@[irreducible]

instance IGame.Dicotic.neg (x : IGame) [x.Dicotic] : (-x).Dicotic

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