mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(set_theory/game/basic): Golf using `antisymmetrization` API

Open vihdzp opened this issue 3 years ago • 4 comments

  • [x] depends on: #13963

I wasn't able to redefine game as antisymmetrization pgame (≤). For whatever reason, that broke a few instances of the ⟦x⟧ notation.

Open in Gitpod

vihdzp avatar May 03 '22 16:05 vihdzp

I'm wondering if we should even have this quotient notation here to begin with? If my rgame definition goes through (briefly discussed on Zulip), we'll have two different instances for pgame.setoid, and that can't be good.

Maybe we could define custom notation ⟦x⟧ᵍ and ⟦x⟧ʳ for these two quotients?

vihdzp avatar May 03 '22 16:05 vihdzp

I can't quite see any more golfing opportunities myself. Care to help a bit?

vihdzp avatar May 03 '22 18:05 vihdzp

Also, what would be a good name for the map from pgame to game? Does game.mk suffice?

vihdzp avatar May 03 '22 18:05 vihdzp

This PR/issue depends on:

  • ~~leanprover-community/mathlib#13963~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar May 15 '22 02:05 mathlib-dependent-issues-bot