-
Notifications
You must be signed in to change notification settings - Fork 298
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/zorn): Added some results about chains #10658
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
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.
Your variable names are a bit confusing but that's just style.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
LGTM. Thanks! bors merge |
Added `chain_empty`, `chain_subsingleton`, and `chain.max_chain_of_chain`. The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle.
Build failed (retrying...): |
Added `chain_empty`, `chain_subsingleton`, and `chain.max_chain_of_chain`. The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle.
Build failed (retrying...): |
bors r- |
Canceled. |
Please merge |
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
Sorry this is the change to implicitness arguments to |
bors r+ |
Added `chain_empty`, `chain_subsingleton`, and `chain.max_chain_of_chain`. The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Added
chain_empty
,chain_subsingleton
, andchain.max_chain_of_chain
.The first two of these are immediate yet useful lemmas. The last one is a consequence of Zorn's lemma, which generalizes Hausdorff's maximality principle.