Commit 2023-07-01 19:42 4e0c38f5

View on Github →

feat: port SetTheory.Game.Short (#5551)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Short.lean

added def PGame.Short.mk'

added def PGame.Short.ofIsEmpty

added inductive PGame.Short

added def PGame.fintypeLeft

added def PGame.fintypeRight

added def PGame.leLfDecidable

added def PGame.moveLeftShort'

added def PGame.moveRightShort'

added def PGame.shortOfRelabelling

added theorem PGame.short_birthday

added theorem PGame.subsingleton_short_example