-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(set_theory/game/*): Protect ambiguous lemmas #13557
Conversation
This PR/issue depends on:
|
I merged with master, since #13530 was just merged. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Protect `pgame.neg_zero` and inline `pgame.add_le_add_left` and friends into `covariant_class` instances. Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Pull request successfully merged into master. Build succeeded: |
@@ -152,7 +152,7 @@ lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G := | |||
by rw [le_zero_iff_zero_le_neg, le_congr (equiv_refl 0) (neg_equiv_self G)] | |||
|
|||
lemma lt_zero_iff {G : pgame} [G.impartial] : G < 0 ↔ 0 < G := | |||
by rw [lt_iff_neg_gt, neg_zero, lt_congr (equiv_refl 0) (neg_equiv_self G)] | |||
by rw [lt_iff_neg_gt, pgame.neg_zero, lt_congr (equiv_refl 0) (neg_equiv_self G)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
why does pgame
have its own neg_zero
? do neither neg_zero
nor neg_zero'
work for it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, pgame
is pretty badly behaved. Most results about pgame
are not equalities but double inequalities (a ≤ b ∧ b ≤ a
instead of a = b
). pgame.neg_zero
is actually the exception here. Once you take the antisymmetrization
, you get game
, which is much saner.
Protect
pgame.neg_zero
and inlinepgame.add_le_add_left
and friends intocovariant_class
instances.