[Merged by Bors] - feat(order/directed): Scott continuous functions by mans0954 · Pull Request #18517 · leanprover-community/mathlib3

mans0954 · 2023-02-28T22:43:06Z

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 (see also #18448).

Holding PR for mathlib4: leanprover-community/mathlib4#2543

YaelDillies · 2023-03-01T01:04:04Z

@vihdzp, any chance this interacts positively with ordinal.is_normal?

vihdzp · 2023-03-01T08:28:07Z

Ordinal functions are strictly monotone, but this might still come in handy for some ordinal results.

src/order/directed.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

This reverts commit 7046749.

src/order/directed.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser

I pushed a handful of golfs.

src/order/directed.lean

mans0954 · 2023-03-12T20:06:18Z

I pushed a handful of golfs.

Thank you!

eric-wieser

bors d+

bors · 2023-04-19T18:50:16Z

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/order/directed.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mans0954 · 2023-04-20T05:36:09Z

Lint seems to be failing in CI due to apt being unable to retrieve a package:

Err:6 http://azure.archive.ubuntu.com/ubuntu jammy-updates/main amd64 libgs9-common all 9.55.0~dfsg1-0ubuntu5.1
  404  Not Found [IP: 40.119.46.219 80]
Err:10 http://azure.archive.ubuntu.com/ubuntu jammy-updates/main amd64 libgs9 amd64 9.55.0~dfsg1-0ubuntu5.1
  404  Not Found [IP: 40.119.46.219 80]
Fetched 59.5 MB in 4s (16.8 MB/s)
E: Failed to fetch http://azure.archive.ubuntu.com/ubuntu/pool/main/g/ghostscript/libgs9-common_9.55.0%7edfsg1-0ubuntu5.1_all.deb  404  Not Found [IP: 40.119.46.219 80]
E: Failed to fetch http://azure.archive.ubuntu.com/ubuntu/pool/main/g/ghostscript/libgs9_9.55.0%7edfsg1-0ubuntu5.1_amd64.deb  404  Not Found [IP: 40.119.46.219 80]
E: Unable to fetch some archives, maybe run apt-get update or try with --fix-missing?
Error: Process completed with exit code 100.

I've tried re-running a couple of times, but always the same result.

mans0954 · 2023-04-20T06:07:25Z

Lint seems to be failing in CI due to apt being unable to retrieve a package:

Merging latest master seems to have fixed it.

YaelDillies · 2023-04-20T07:55:04Z

Yeah, this was fixed on Zulip a few days ago.

mans0954 · 2023-04-20T09:06:38Z

bors r+

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>

bors · 2023-04-20T14:40:18Z

Pull request successfully merged into master.

Build succeeded:

mans0954 · 2023-04-20T18:51:09Z

@YaelDillies , @eric-wieser - for the Mathlib4 port, should I expect the equivalent file in mathlib3port to get updated automatically? (This doesn't seem to have happened yet.)

YaelDillies · 2023-04-20T19:23:10Z

Yes, it will happen in about 8 hours from now.

mans0954 · 2023-04-20T19:31:44Z

Yes, it will happen in about 8 hours from now.

Thanks - and then I manually copy over the changes into leanprover-community/mathlib4#2543, fixing any issues as necessary?

YaelDillies · 2023-04-20T19:38:08Z

Yes, exactly. Also note that you don't need to fetch the changes yourself. You can just wait for the bump to nightly-2023-04-21-04 (or something like that) entry in the mathlib3port column at https://leanprover-community.github.io/mathlib-port-status/file/order/directed to appear.

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>

…lies OmegaCompletePartialOrder.Continuous' (#6831) In leanprover-community/mathlib3#18517 we introduced the notion of a Scott Continuous function between preorders. This PR shows that a Scott Continuous function between OmegaCompletePartialOrders is necessarily `OmegaCompletePartialOrder.Continuous'`. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

mans0954 added 2 commits February 28, 2023 22:22

Add some results for directed_on and reflexive relations

a0bcf89

A function that preserves lub on directed sets is monotone

0efadbf

mans0954 requested a review from YaelDillies February 28, 2023 22:43

This was referenced Feb 28, 2023

[Merged by Bors] - feat: forward-port leanprover-community/mathlib#18517 leanprover-community/mathlib4#2543

Closed

[Merged by Bors] - feat: Scott topology on a preorder leanprover-community/mathlib4#2508

Closed

mans0954 added the awaiting-review The author would like community review of the PR label Mar 1, 2023

eric-wieser reviewed Mar 2, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 2, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 2, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 2, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

mans0954 and others added 6 commits March 2, 2023 18:49

Update src/order/directed.lean

13522e2

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update src/order/directed.lean

4b681ec

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Counter example

7046749

Revert "Counter example"

dd2379f

This reverts commit 7046749.

Better variable names

f9652f0

More better variable names

6580139

eric-wieser reviewed Mar 11, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 11, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

mans0954 and others added 5 commits March 11, 2023 20:53

Update src/order/directed.lean

7229d3a

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update src/order/directed.lean

6312ff7

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

golfs

2269de2

golf

6f4e919

docstring

20ea369

eric-wieser reviewed Mar 12, 2023

View reviewed changes

lintfix

854c814

eric-wieser reviewed Mar 12, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

kim-em added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 28, 2023

eric-wieser approved these changes Apr 19, 2023

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 19, 2023

mans0954 and others added 3 commits April 19, 2023 20:21

Update src/order/directed.lean

46df244

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Add to docstring

7a74b60

Add reference

62248c3

YaelDillies reviewed Apr 19, 2023

View reviewed changes

src/order/directed.lean Outdated Show resolved Hide resolved

Update src/order/directed.lean

3d2aa3f

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge branch 'master' into mans0954/directed-on-insert

2e055d3

bors bot changed the title ~~feat(order/directed): Scott continuous functions~~ [Merged by Bors] - feat(order/directed): Scott continuous functions Apr 20, 2023

bors bot closed this Apr 20, 2023

bors bot deleted the mans0954/directed-on-insert branch April 20, 2023 14:40

mans0954 mentioned this pull request Aug 28, 2023

[Merged by Bors] - feat(Order/OmegaCompletePartialOrder): Show that Scott Continuity implies OmegaCompletePartialOrder.Continuous' leanprover-community/mathlib4#6831

Closed

Conversation

mans0954 commented Feb 28, 2023 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Mar 1, 2023

Uh oh!

vihdzp commented Mar 1, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mans0954 commented Mar 12, 2023

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

bors bot commented Apr 19, 2023

Uh oh!

Uh oh!

mans0954 commented Apr 20, 2023

Uh oh!

mans0954 commented Apr 20, 2023

Uh oh!

YaelDillies commented Apr 20, 2023

Uh oh!

mans0954 commented Apr 20, 2023

Uh oh!

bors bot commented Apr 20, 2023

Uh oh!

mans0954 commented Apr 20, 2023

Uh oh!

YaelDillies commented Apr 20, 2023

Uh oh!

mans0954 commented Apr 20, 2023

Uh oh!

YaelDillies commented Apr 20, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

mans0954 commented Feb 28, 2023 •

edited by YaelDillies

Loading