[Merged by Bors] - feat(order/directed): Scott continuous functions

[mans0954]

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]

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

[vihdzp]

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

[eric-wieser]

I pushed a handful of golfs.

[mans0954]

I pushed a handful of golfs.

Thank you!

[eric-wieser]

bors d+

[bors]

✌️ 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.

[mans0954]

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]

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]

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

[mans0954]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[mans0954]

@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]

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

[mans0954]

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]

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.