Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-28 10:11 8900d545

View on Github →

feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (#15260)

Estimated changes

Modified src/set_theory/game/basic.lean

added theorem game.bdd_above_of_small

added theorem game.bdd_below_of_small

Modified src/set_theory/game/pgame.lean

added theorem pgame.bdd_above_of_small

added theorem pgame.bdd_below_of_small

added theorem pgame.le_upper_bound

added def pgame.lower_bound

added theorem pgame.lower_bound_le

added theorem pgame.lower_bound_mem_lower_bounds

added def pgame.upper_bound

added theorem pgame.upper_bound_mem_upper_bounds

Modified src/set_theory/surreal/basic.lean

added theorem surreal.bdd_above_of_small

added theorem surreal.bdd_below_of_small

added theorem surreal.lower_bound_numeric

added theorem surreal.upper_bound_numeric