Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 03:13 a16f1cfe

View on Github →

feat(set_theory/game/basic): cast inequalities on pgame to game (#14405)

Estimated changes

Modified src/set_theory/game/basic.lean

added theorem pgame.equiv_iff_game_eq

added theorem pgame.fuzzy_iff_game_fuzzy

added theorem pgame.le_iff_game_le

added theorem pgame.lf_iff_game_lf

added theorem pgame.lt_iff_game_lt