-
Notifications
You must be signed in to change notification settings - Fork 297
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] - feat(analysis/convex/[basic, topology]): generalize path connectedness of convex sets to topological real vector spaces #10011
Conversation
ADedecker
commented
Oct 27, 2021
The linter is not happy. Do you understand what is going on? |
First, sorry for the late response. I'm not sure what precisely goes wrong, but what I understand is that Lean tries a lot of things to prove that a product type is nonempty without the assumption that each factor is. One of them is trying to prove path connectedness, and somehow generalizing this instance makes the search significantly slower. So I guess the fix would be to lower a priority somewhere, but I have no idea where exactly. |
As suggested here, I increased the acceptable limit for the |
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
…s of convex sets to topological real vector spaces (#10011)
Pull request successfully merged into master. Build succeeded: |
…s of convex sets to topological real vector spaces (#10011)