Mathlib v3 is deprecated. Go to Mathlib v4

Theorem surreal.upper_bound_numeric

Modification history

2023-07-28 10:11
src/set_theory/surreal/basic.lean
feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (#15260)
Added surreal.upper_bound_numericView on Github →