Commit 2024-12-21 03:42 839e3f6b

View on Github →

feat(SetTheory/Game/PGame): down and up games (#19393) Implements definitions for up and down games, their negations, and their inequivalence to 0.

Estimated changes

Modified Mathlib/SetTheory/Game/PGame.lean

added def SetTheory.PGame.down

added theorem SetTheory.PGame.down_leftMoves

added theorem SetTheory.PGame.down_moveLeft

added theorem SetTheory.PGame.down_moveRight

added theorem SetTheory.PGame.down_neg

added theorem SetTheory.PGame.down_rightMoves

added theorem SetTheory.PGame.neg_down

added theorem SetTheory.PGame.neg_up

added theorem SetTheory.PGame.star_fuzzy_down

added theorem SetTheory.PGame.star_fuzzy_up

added def SetTheory.PGame.up

added theorem SetTheory.PGame.up_leftMoves

added theorem SetTheory.PGame.up_moveLeft

added theorem SetTheory.PGame.up_moveRight

added theorem SetTheory.PGame.up_neg

added theorem SetTheory.PGame.up_rightMoves