-
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(order/partition/finpartition): Finite partitions #9795
Conversation
This should be mentioned in |
Small bump on this, do you need any help with filling in the gaps? |
Yes please! My plan is to build the infimum and supremum of finpartitions to demonstrate the benefit of not indexing them. It's not strictly necessary for the rest of Szemerédi but rather a matter of whether @eric-wieser is already convinced or not. |
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, but I didn't try out the API myself yet. @eric-wieser any final comments?
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
This defines finite partitions along with quite a few constructions, Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This defines finite partitions along with quite a few constructions,
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com
set.pairwise_disjoint
#9898set.pairwise_disjoint
withfinset
#10244