Theorem Surreal.bddBelow_of_small

Modification history

2026-02-20 00:22
Mathlib/SetTheory/Surreal/Basic.lean
chore: remove deprecated material from CGT (#35550) …
Deleted Surreal.bddBelow_of_smallView on Github →
2024-03-09 22:29
Mathlib/SetTheory/Surreal/Basic.lean
feat: Small sets of games/surreals are bounded (#10458) …
Added Surreal.bddBelow_of_smallView on Github →