SetTheory.Game.Pgame: Equiv / Identical on Left/Right

Stream: mathlib4

[Tristan Figueroa-Reid]

Would having specific equivalence relations for left and right sets be helpful? While writing theorem neg_identical_neg_iff : ∀ {x y : PGame.{u}}, x ≡ y ↔ -x ≡ -y, it felt worthwhile to have an IdenticalLeft/IdenticalRight distinction, but it could be due to my inexperience with formalization.

[Tristan Figueroa-Reid]

I did figure out a way to do this much more nicely without any Left/Right variants of equivalence, but I'll still leave this thread open, because I am curious about why this would be a bad/good idea!

[Violeta Hernández]

Hey! I'm like one of two active contributors to game theory at the moment, so if you have any questions related to that you should ping me on here.

[Violeta Hernández]

What do you mean by IdenticalLeft and IdenticalRight? Is that just "the game with only x's left options is identical to the game with only y's left options"?

[Tristan Figueroa-Reid]

Violeta Hernández said:

Hey! I'm like one of two active contributors to game theory at the moment, so if you have any questions related to that you should ping me on here.

Sorry about the lack of pings! I constantly forget that this environment is extremely busy and it's hard to check every message on here.

I do just mean the game with only x's left options is identical to the game with only y's left options and vice versa for right, though my opinion on having that has changed since I asked this question.