Theorem Ordinal.toGame_lf_iff

Modification history

2025-01-02 23:22

Mathlib/SetTheory/Game/Ordinal.lean

chore(SetTheory/Game/Ordinal): make `Ordinal.toGame` an order embedding (#19417) …

Modified Ordinal.toGame_lf_iff View on Github →

2024-11-14 00:03

Mathlib/SetTheory/Game/Ordinal.lean

feat(SetTheory/Game/Birthday): basic API for `Ordinal.toGame` (#17015)

Added Ordinal.toGame_lf_iff View on Github →