# mathlibdocumentation

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 (G : pgame) :
Prop

The player who goes first loses

Equations
def pgame.first_wins (G : pgame) :
Prop

The player who goes first wins

Equations
def pgame.left_wins (G : pgame) :
Prop

The left player can always win

Equations
def pgame.right_wins (G : pgame) :
Prop

The right player can always win

Equations
theorem pgame.first_loses_of_equiv {G H : pgame} (h : G.equiv H) :

theorem pgame.first_wins_of_equiv {G H : pgame} (h : G.equiv H) :

theorem pgame.left_wins_of_equiv {G H : pgame} (h : G.equiv H) :

theorem pgame.right_wins_of_equiv {G H : pgame} (h : G.equiv H) :

theorem pgame.first_loses_of_equiv_iff {G H : pgame} (h : G.equiv H) :

theorem pgame.first_wins_of_equiv_iff {G H : pgame} (h : G.equiv H) :

theorem pgame.left_wins_of_equiv_iff {G H : pgame} (h : G.equiv H) :

theorem pgame.right_wins_of_equiv_iff {G H : pgame} (h : G.equiv H) :