We've defined a bunch of order relations on PGame which are really just special cases of other relations on pre/partial orders. This issue keeps track of which of them are yet to be removed/generalized.

• SetTheory.PGame.LF is the same as ¬ b ≤ a
  • Deprecate LF
• SetTheory.PGame.Equiv is the same as AntisymmRel
  • Copy over the Equiv API to AntisymmRel: [Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas #19571
  • Deprecate Equiv: chore(SetTheory/Game/PGame): Equiv → AntisymmRel #21086
• SetTheory.Game.Fuzzy is the incomparability relation.
  • Add IncompRel: [Merged by Bors] - feat(Order/Comparable): comparability/incomparability relations #19580
  • Deprecate Fuzzy