Commit 2024-03-09 22:29 d004cbb5
View on Github →feat: Small sets of games/surreals are bounded (#10458)
Finish forwarding porting https://github.com/leanprover-community/mathlib/pull/15260 after #10566 ported just the changes in PGame.lean.
We don't port upper_bound_numeric (or lower_bound_numeric) because upper_bound was deleted following review feedback on the previous forward-porting PR #10566.