Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 21:01 178456ff

View on Github →

feat(set_theory/surreal/basic): definition of ≤ and < on numeric games (#14169)

Estimated changes

added theorem pgame.le_iff_forall_lt
added theorem pgame.le_of_forall_lt
added theorem pgame.lt_def
added theorem pgame.lt_iff_forall_le
added theorem pgame.lt_of_forall_le