Commit 2023-07-01 23:04 b411eb9c

View on Github →

feat: port SetTheory.Game.State (#5653)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/State.lean

added def Game.ofState

added def PGame.leftMovesOfState

added def PGame.leftMovesOfStateAux

added def PGame.ofState

added def PGame.ofStateAux

added def PGame.ofStateAuxRelabelling

added def PGame.relabellingMoveLeft

added def PGame.relabellingMoveLeftAux

added def PGame.relabellingMoveRight

added def PGame.relabellingMoveRightAux

added def PGame.rightMovesOfState

added def PGame.rightMovesOfStateAux

added theorem PGame.turnBound_ne_zero_of_left_move

added theorem PGame.turnBound_ne_zero_of_right_move

added theorem PGame.turnBound_of_left

added theorem PGame.turnBound_of_right