Commit 2022-03-29 05:57 5fb7b7b6

View on Github →

feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659) We define mex and bmex, and use the former to golf the proof of Sprague-Grundy.

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

deleted theorem cardinal.mk_ordinal_out

Modified src/set_theory/game/nim.lean

modified theorem pgame.grundy_value_nim_add_nim

deleted def pgame.nonmoves

deleted theorem pgame.nonmoves_nonempty

Modified src/set_theory/ordinal.lean

added theorem cardinal.mk_ordinal_out

Modified src/set_theory/ordinal_arithmetic.lean

added def ordinal.bmex

added theorem ordinal.bmex_le_blsub

added theorem ordinal.bmex_le_of_ne

added theorem ordinal.bmex_lt_ord_succ_card

added theorem ordinal.bmex_monotone

added theorem ordinal.bmex_not_mem_brange

added theorem ordinal.exists_of_lt_bmex

added theorem ordinal.exists_of_lt_mex

deleted theorem ordinal.lsub_nmem_range

added theorem ordinal.lsub_not_mem_range

added def ordinal.mex

added theorem ordinal.mex_le_lsub

added theorem ordinal.mex_le_of_ne

added theorem ordinal.mex_lt_ord_succ_mk

added theorem ordinal.mex_monotone

added theorem ordinal.mex_not_mem_range

added theorem ordinal.ne_bmex

added theorem ordinal.ne_mex

added theorem ordinal.nonempty_compl_range