[Merged by Bors] - feat: forward-port leanprover-community/mathlib#18517#2543
Closed
[Merged by Bors] - feat: forward-port leanprover-community/mathlib#18517#2543
Conversation
3 tasks
bors bot
pushed a commit
to leanprover-community/mathlib3
that referenced
this pull request
Apr 20, 2023
We prove an insert result for directed sets when the relation is reflexive. This is then used to show that a Scott continuous function is monotone. This result is required in the [construction of the Scott topology on a preorder](leanprover-community/mathlib4#2508) (see also #18448). Holding PR for mathlib4: leanprover-community/mathlib4#2543 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
91a801a to
a424a69
Compare
This one-line change lets us forward-port this other PR simultaneously.
Member
|
leanprover-community/mathlib3#8475 isn't through mathport yet. Are you sure this ports it? |
eric-wieser
reviewed
Apr 21, 2023
Mathlib/Order/Directed.lean
Outdated
|
|
||
| ! This file was ported from Lean 3 source module order.directed | ||
| ! leanprover-community/mathlib commit 18a5306c091183ac90884daa9373fa3b178e8607 | ||
| ! leanprover-community/mathlib commit e8cf0cfec5fcab9baf46dc17d30c5e22048468be |
Member
There was a problem hiding this comment.
Are you sure you don't mean leanprover-community/mathlib3@485b24e?
Collaborator
Author
There was a problem hiding this comment.
@eric-wieser The diff here says:
-! leanprover-community/mathlib commit 485b24ed47b1b7978d38a1e445158c6224c3f42c
+! leanprover-community/mathlib commit e8cf0cfec5fcab9baf46dc17d30c5e22048468be
So I assumed e8cf0cfec5fcab9baf46dc17d30c5e22048468be was the new value to use?
Contributor
There was a problem hiding this comment.
I was the one updating the SHA to this. It should be the right value.
Member
There was a problem hiding this comment.
I backed this change out anyway because it's less confusing to port it in #3588.
@mans0954: the dashboard presents multiple diffs; an overall diff, and a diff per commit. I was confused because your PR title suggested this was for just one commit. In general, prefer porting one commit at a time because it's easier for reviewers to diff against the mathport output in the dashboard, and gives a cleaner git history.
1 task
Contributor
It's a one-line change, so yes. |
It's easier to revert this change than come up with a sensible title for this PR. We can forward-port this single line along with the rest of leanprover-community/mathlib3#8475
Member
|
bors d+ |
|
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
Collaborator
Author
|
bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Apr 24, 2023
Matches leanprover-community/mathlib3#18517 This result is required in #2508. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
kim-em
pushed a commit
that referenced
this pull request
May 10, 2023
Matches leanprover-community/mathlib3#18517 This result is required in #2508. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 10, 2023
Matches leanprover-community/mathlib3#18517 This result is required in #2508. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 11, 2023
Matches leanprover-community/mathlib3#18517 This result is required in #2508. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Matches leanprover-community/mathlib3#18517
This result is required in #2508.
We prove an insert result for directed sets when the relation is reflexive. This is then used to show that a Scott continuous function is monotone.