-
Notifications
You must be signed in to change notification settings - Fork 299
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] - refactor(set_theory/game/*): fix theorem names #14685
Conversation
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.
LGTM, thanks! Strangely "build mathlib" failed without showing error messages...
|
Thanks! bors merge |
Some theorems about `exists` had `forall` in the name, other theorems about swapped `≤` or `⧏` used `le` and `lf` instead of `ge` and `gf`. We also golf `le_of_forall_lt`.
Build failed (retrying...): |
Some theorems about `exists` had `forall` in the name, other theorems about swapped `≤` or `⧏` used `le` and `lf` instead of `ge` and `gf`. We also golf `le_of_forall_lt`.
Build failed (retrying...): |
Canceled. |
CI has now passed and I think it's time to request another |
bors merge |
Some theorems about `exists` had `forall` in the name, other theorems about swapped `≤` or `⧏` used `le` and `lf` instead of `ge` and `gf`. We also golf `le_of_forall_lt`. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Some theorems about
exists
hadforall
in the name, other theorems about swapped≤
or⧏
usedle
andlf
instead ofge
andgf
.We also golf
le_of_forall_lt
.