Commit 2024-08-11 23:33 52853729

View on Github →

chore(SetTheory/Game/Basic): fix Game.PGame namespace (#15708) We move the Fuzzy definition so that the PGame namespace doesn't need to be opened twice. We also move the infix notation definition a bit later down the file.

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

deleted theorem SetTheory.Game.PGame.equiv_iff_game_eq

deleted theorem SetTheory.Game.PGame.fuzzy_iff_game_fuzzy

deleted theorem SetTheory.Game.PGame.le_iff_game_le

deleted theorem SetTheory.Game.PGame.lf_iff_game_lf

deleted theorem SetTheory.Game.PGame.lt_iff_game_lt

modified theorem SetTheory.Game.not_le

modified theorem SetTheory.Game.not_lf

added theorem SetTheory.PGame.equiv_iff_game_eq

added theorem SetTheory.PGame.fuzzy_iff_game_fuzzy

added theorem SetTheory.PGame.le_iff_game_le

added theorem SetTheory.PGame.lf_iff_game_lf

added theorem SetTheory.PGame.lt_iff_game_lt

Modified Mathlib/SetTheory/Game/Impartial.lean