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

Prop

The player who goes first loses

Equations

G.first_loses = (G ≤ 0 ∧ 0 ≤ G)

def pgame.first_wins (G : pgame) :

Prop

The player who goes first wins

Equations

G.first_wins = (0 < G ∧ G < 0)

def pgame.left_wins (G : pgame) :

Prop

The left player can always win

Equations

G.left_wins = (0 < G ∧ 0 ≤ G)

def pgame.right_wins (G : pgame) :

Prop

The right player can always win

Equations

G.right_wins = (G ≤ 0 ∧ G < 0)

theorem pgame.zero_first_loses :

theorem pgame.one_left_wins :

theorem pgame.star_first_wins :

pgame.star.first_wins

theorem pgame.omega_left_wins :

pgame.omega.left_wins

theorem pgame.winner_cases (G : pgame) :

G.left_wins ∨ G.right_wins ∨ G.first_loses ∨ G.first_wins

theorem pgame.first_loses_is_zero {G : pgame} :

G.first_loses ↔ G.equiv 0

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

G.first_loses → H.first_loses

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

G.first_wins → H.first_wins

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

G.left_wins → H.left_wins

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

G.right_wins → H.right_wins

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

G.first_loses ↔ H.first_loses

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

G.first_wins ↔ H.first_wins

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

G.left_wins ↔ H.left_wins

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

G.right_wins ↔ H.right_wins

theorem pgame.not_first_wins_of_first_loses {G : pgame} :

G.first_loses → ¬G.first_wins

theorem pgame.not_first_loses_of_first_wins {G : pgame} :

G.first_wins → ¬G.first_loses