Commit 2025-03-20 10:32 79c27b32

View on Github →

chore: split SetTheory.Game.PGame (#23133)

  • SetTheory.PGame.Basic contains basic definitions, relabelling and option insertion.
  • SetTheory.PGame.Order contains order-related definitions.
  • SetTheory.PGame.Algebra contains pregame addition and subtraction and negation, and associated lemmas.

Estimated changes

deleted theorem LE.le.not_gf
deleted theorem SetTheory.PGame.Equiv.ge
deleted theorem SetTheory.PGame.Equiv.le
deleted inductive SetTheory.PGame.IsOption
deleted theorem SetTheory.PGame.LF.not_ge
deleted theorem SetTheory.PGame.LF.not_gt
deleted def SetTheory.PGame.LF
deleted inductive SetTheory.PGame.Relabelling
deleted theorem SetTheory.PGame.add_congr
deleted theorem SetTheory.PGame.down_neg
deleted theorem SetTheory.PGame.equiv_def
deleted theorem SetTheory.PGame.equiv_rfl
deleted theorem SetTheory.PGame.ext
deleted theorem SetTheory.PGame.le_congr
deleted theorem SetTheory.PGame.le_def
deleted theorem SetTheory.PGame.le_or_gf
deleted theorem SetTheory.PGame.le_zero
deleted theorem SetTheory.PGame.lf_congr
deleted theorem SetTheory.PGame.lf_def
deleted theorem SetTheory.PGame.lf_irrefl
deleted theorem SetTheory.PGame.lf_mk
deleted theorem SetTheory.PGame.lf_of_lt
deleted theorem SetTheory.PGame.lf_zero
deleted theorem SetTheory.PGame.lt_congr
deleted theorem SetTheory.PGame.mk_le_mk
deleted theorem SetTheory.PGame.mk_lf
deleted theorem SetTheory.PGame.mk_lf_mk
deleted def SetTheory.PGame.neg
deleted theorem SetTheory.PGame.neg_def
deleted theorem SetTheory.PGame.neg_down
deleted theorem SetTheory.PGame.neg_star
deleted theorem SetTheory.PGame.neg_up
deleted theorem SetTheory.PGame.not_lf
deleted theorem SetTheory.PGame.sub_congr
deleted def SetTheory.PGame.up
deleted theorem SetTheory.PGame.up_neg
deleted theorem SetTheory.PGame.zero_le
deleted theorem SetTheory.PGame.zero_lf
deleted inductive SetTheory.PGame
added theorem SetTheory.PGame.neg_up
added theorem SetTheory.PGame.up_neg
added inductive SetTheory.PGame.IsOption
added theorem SetTheory.PGame.ext
added inductive SetTheory.PGame
added theorem LE.le.not_gf
added theorem SetTheory.PGame.le_def
added theorem SetTheory.PGame.lf_def
added theorem SetTheory.PGame.lf_mk
added theorem SetTheory.PGame.mk_lf
added theorem SetTheory.PGame.not_lf