Commit 2023-06-27 07:58 0894eca6

View on Github →

feat: port SetTheory.Surreal.Basic (#5515)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Surreal/Basic.lean

added theorem PGame.Numeric.add

added theorem PGame.Numeric.le_moveRight

added theorem PGame.Numeric.left_lt_right

added theorem PGame.Numeric.lt_moveRight

added theorem PGame.Numeric.mk

added theorem PGame.Numeric.moveLeft

added theorem PGame.Numeric.moveLeft_le

added theorem PGame.Numeric.moveLeft_lt

added theorem PGame.Numeric.moveRight

added theorem PGame.Numeric.neg

added theorem PGame.Numeric.sub

added def PGame.Numeric

added theorem PGame.Relabelling.numeric_congr

added theorem PGame.Relabelling.numeric_imp

added theorem PGame.le_iff_forall_lt

added theorem PGame.le_of_lf

added theorem PGame.lf_asymm

added theorem PGame.lf_iff_lt

added theorem PGame.lt_def

added theorem PGame.lt_iff_exists_le

added theorem PGame.lt_of_exists_le

added theorem PGame.lt_of_lf

added theorem PGame.lt_or_equiv_or_gt

added theorem PGame.not_fuzzy

added theorem PGame.numeric_def

added theorem PGame.numeric_nat

added theorem PGame.numeric_of_isEmpty

added theorem PGame.numeric_of_isEmpty_leftMoves

added theorem PGame.numeric_of_isEmpty_rightMoves

added theorem PGame.numeric_one

added theorem PGame.numeric_rec

added theorem PGame.numeric_toPGame

added theorem PGame.numeric_zero

added def Surreal.lift

added def Surreal.lift₂

added def Surreal.mk

added theorem Surreal.nat_toGame

added theorem Surreal.one_toGame

added def Surreal.toGame

added theorem Surreal.zero_toGame

added def Surreal