Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(order/locally_finite): finset.interval #17939

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(order/locally_finite): finset.interval #17939

wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 14, 2022 •
edited by github-actions bot

A finset-valued version of set.interval.

I need this for the proof of the van den Berg-Kesten-Reimer inequality on page 2.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. t-order Order hierarchy labels Dec 14, 2022
@YaelDillies YaelDillies added this to van den Berg-Kesten-Reimer in Correlation inequalities Dec 14, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Dec 15, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

eric-wieser
eric-wieser reviewed Dec 16, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a 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?

@eric-wieser
Copy link
Member

I think at least one of these files should have a docstring that mentions the new interval too.

@eric-wieser
Copy link
Member

Probably you should look at every locally_finite_order instance, and add interval lemmas if there are already Icc lemmas nearby.

@YaelDillies
Copy link
Collaborator Author

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?

@ocfnash
Copy link
Collaborator

ocfnash commented Dec 26, 2022

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 26, 2022
bors bot pushed a commit that referenced this pull request Dec 26, 2022
@YaelDillies
feat(order/locally_finite): finset.interval (#17939)
a7b9272 
A `finset`-valued version of `set.interval`.
@bors
Copy link

bors bot commented Dec 26, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/locally_finite): finset.interval [Merged by Bors] - feat(order/locally_finite): finset.interval Dec 26, 2022
@bors bors bot closed this Dec 26, 2022
@bors bors bot deleted the finset_interval branch December 26, 2022 21:32
@YaelDillies YaelDillies mentioned this pull request Apr 19, 2023
Closed
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-order Order hierarchy
Projects
Correlation inequalities
van den Berg-Kesten-Reimer
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@YaelDillies @mathlib-dependent-issues-bot @eric-wieser @ocfnash