-
Notifications
You must be signed in to change notification settings - Fork 234
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: missing API lemmas about the prod instance in Order/CompleteLattice #1369
Conversation
Thanks for doing this, but I think it would be best to wait for mathport to run and discard the manual port in favor of the automatic one. There are some ongoing discussions on Zulip about that. |
https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Order/CompleteLattice.lean should be ready in about 4 hours |
b248c5c
to
cdee174
Compare
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.
LTGM
bors merge |
…tice (#1369) This adds lemmas about how `fst`, `snd`, and `swap` interact with `supₛ` and `infₛ`. Manual port of a [mathlib PR](leanprover-community/mathlib#18029) by @eric-wieser Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Whoops, we forgot to update the SHA here. |
This adds lemmas about how
fst
,snd
, andswap
interact withsupₛ
andinfₛ
.Manual port of leanprover-community/mathlib#18029 by @eric-wieser