pgame): `ordinal.to_pgame` (#13628)

Commit

3 years ago

feat(set_theory/game/pgame): `ordinal.to_pgame` (#13628) We define the canonical map from ordinals to pre-games and prove it's an order embedding.

Author

vihdzp

Parents