Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-17 17:38 901178e2

View on Github →

feat(set_theory/surreal): surreal numbers (#958)

  • feat(set_theory/surreal): surreal numbers
  • doc(set_theory/surreal): surreal docs
  • minor changes in surreal

Estimated changes

added def pSurreal.add
added def pSurreal.equiv
added theorem pSurreal.equiv_refl
added theorem pSurreal.equiv_symm
added theorem pSurreal.equiv_trans
added def pSurreal.inv'
added def pSurreal.inv_val
added theorem pSurreal.le_congr
added def pSurreal.le_lt
added theorem pSurreal.le_of_lt
added theorem pSurreal.le_refl
added theorem pSurreal.le_trans
added theorem pSurreal.le_trans_aux
added theorem pSurreal.lt_asymm
added theorem pSurreal.lt_congr
added theorem pSurreal.lt_irrefl
added theorem pSurreal.lt_mk_of_le
added theorem pSurreal.lt_of_le_mk
added theorem pSurreal.lt_of_mk_le
added theorem pSurreal.mk_le_mk
added theorem pSurreal.mk_lt_mk
added theorem pSurreal.mk_lt_of_le
added def pSurreal.mul
added theorem pSurreal.ne_of_lt
added def pSurreal.neg
added theorem pSurreal.not_le
added theorem pSurreal.not_le_lt
added theorem pSurreal.not_lt
added def pSurreal.ok
added theorem pSurreal.ok_rec
added def pSurreal.omega
added inductive pSurreal.{u}
added def surreal.equiv
added def surreal.le
added def surreal.lift
added def surreal.lift₂
added def surreal.lt
added def surreal.mk
added theorem surreal.not_le
added def surreal
added inductive {u}