-
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/locally_finite): finset.interval
#17939
Conversation
This PR/issue depends on: |
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.
Since you've added this new def alongside Icc
, can you go through lemma like prod.Icc_eq
and add their interval
counterparts?
I think at least one of these files should have a docstring that mentions the new |
Probably you should look at every |
I've started doing so but the PR would become huge. Do you mind making that a separate PR in order not to block my progress on vdBKR? |
bors merge |
A `finset`-valued version of `set.interval`.
Pull request successfully merged into master. Build succeeded: |
finset.interval
finset.interval
A
finset
-valued version ofset.interval
.I need this for the proof of the van den Berg-Kesten-Reimer inequality on page 2.