Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pgame.lower_bound_mem_lower_bounds

Modification history

2023-07-28 10:11

src/set_theory/game/pgame.lean

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

Added pgame.lower_bound_mem_lower_bounds View on Github →