Commit 2024-02-28 16:59 74460c6f

View on Github →

feat(SetTheory): Upper bound for games (#10566) Partially forward-port https://github.com/leanprover-community/mathlib/pull/15260

Estimated changes

Modified Mathlib/SetTheory/Game/PGame.lean

added theorem SetTheory.PGame.bddAbove_of_small

added theorem SetTheory.PGame.bddAbove_range_of_small

added theorem SetTheory.PGame.bddBelow_of_small

added theorem SetTheory.PGame.bddBelow_range_of_small