mathlib documentation

set_theory.game.winner

Basic definitions about who has a winning stratergy

We define G.first_loses, G.first_wins, G.left_wins and G.right_wins for a pgame G, which means the second, first, left and right players have a winning strategy respectively. These are defined by inequalities which can be unfolded with pgame.lt_def and pgame.le_def.

def pgame.first_loses  :
pgame → Prop

The player who goes first loses

Equations
def pgame.first_wins  :
pgame → Prop

The player who goes first wins

Equations
def pgame.left_wins  :
pgame → Prop

The left player can always win

Equations
def pgame.right_wins  :
pgame → Prop

The right player can always win

Equations
theorem pgame.first_wins_of_equiv {G H : pgame} :
G.equiv HG.first_wins → H.first_wins

theorem pgame.left_wins_of_equiv {G H : pgame} :
G.equiv HG.left_wins → H.left_wins

theorem pgame.right_wins_of_equiv {G H : pgame} :
G.equiv HG.right_wins → H.right_wins