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

feat: RBSet.{upperBound?, lowerBound?} lemmas #740

Merged
merged 3 commits into from May 16, 2024
Merged

feat: RBSet.{upperBound?, lowerBound?} lemmas #740

merged 3 commits into from May 16, 2024

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Apr 14, 2024 •
edited

This adds RBSet.upperBound? symmetric to lowerBound?, and lifts all the RBNode theorems to RBSet (and also adds some more).

@digama0 digama0 force-pushed the rbset_upperbound branch 2 times, most recently from 0c532f8 to 7db3d2b Compare April 14, 2024 08:36
@digama0 digama0 mentioned this pull request Apr 16, 2024
Open
5 tasks
@digama0 digama0 added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on another PR This is stacked on top of another Std4 PR. labels Apr 16, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 17, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Apr 17, 2024
@digama0 digama0 removed the depends on another PR This is stacked on top of another Std4 PR. label Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels May 1, 2024
@semorrison semorrison added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label May 13, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 13, 2024
@semorrison semorrison merged commit f635b69 into main May 16, 2024
3 checks passed
@semorrison semorrison deleted the rbset_upperbound branch May 16, 2024 01:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison approved these changes

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@digama0 @semorrison @leanprover-community-mathlib4-bot