Commit 2024-09-18 22:25 6b33760c

View on Github →

chore(SetTheory/Game/Nim): redefine grundyValue as an infimum (#16874) We redefine grundyValue as an infimum instead of using Ordinal.mex, and we give it a better API. This is a preliminary step before deprecating Ordinal.mex altogether - there's no point in using it since we can just use Inf sᶜ instead.

Estimated changes

Modified Mathlib/SetTheory/Game/Nim.lean

deleted theorem SetTheory.PGame.exists_grundyValue_left_of_lt

added theorem SetTheory.PGame.exists_grundyValue_moveLeft_of_lt

added theorem SetTheory.PGame.exists_grundyValue_moveRight_of_lt

deleted theorem SetTheory.PGame.exists_grundyValue_right_of_lt

added theorem SetTheory.PGame.grundyValue_eq_sInf_moveLeft

added theorem SetTheory.PGame.grundyValue_eq_sInf_moveRight

added theorem SetTheory.PGame.grundyValue_le_of_forall_moveLeft

added theorem SetTheory.PGame.grundyValue_le_of_forall_moveRight

deleted theorem SetTheory.PGame.grundyValue_ne_left

added theorem SetTheory.PGame.grundyValue_ne_moveLeft

added theorem SetTheory.PGame.grundyValue_ne_moveRight

deleted theorem SetTheory.PGame.grundyValue_ne_right

modified theorem SetTheory.PGame.grundyValue_nim_add_nim

added theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveLeft

added theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveRight