Commit 2024-07-14 01:42 711980bd

View on Github →

feat(SetTheory/Game/PGame): inserting an option a game (#14517) inserting an option into a game

Estimated changes

Modified Mathlib/SetTheory/Game/PGame.lean

added def SetTheory.PGame.insertLeft

added theorem SetTheory.PGame.insertLeft_equiv_of_lf

added def SetTheory.PGame.insertRight

added theorem SetTheory.PGame.insertRight_equiv_of_lf

added theorem SetTheory.PGame.insertRight_insertLeft

added theorem SetTheory.PGame.insertRight_le

added theorem SetTheory.PGame.le_insertLeft

added theorem SetTheory.PGame.neg_insertLeft_neg

added theorem SetTheory.PGame.neg_insertRight_neg

Modified Mathlib/SetTheory/Surreal/Basic.lean

added theorem SetTheory.PGame.insertLeft_numeric

added theorem SetTheory.PGame.insertRight_numeric