[Merged by Bors] - feat(Topology/Order/UpperLowerSetTopology): Introduce the Upper Set (or Alexandrov) topology and the Lower Set topology by mans0954 · Pull Request #5672 · leanprover-community/mathlib4

mans0954 · 2023-07-02T16:24:57Z

Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology.

An Alexandrov topology is a topology where the intersection of any collection of open sets is open. The UpperSetTopology is an Alexandrov topology, and, given any Alexandrov topology, a Preorder may be defined on the underlying set such that the UpperSetTopology of the Preorder coincides with the original topology.

However, our motivation for introducing the UpperSetTopology is its use in the construction of the Scott Topology (#2508). Beyond demonstrating that the set of open sets is closed under arbitrary intersections, we have not sought to further develop the theory of Alexandrov topologies in this PR. However, we hope that by breaking the Upper Set topology out into a separate file / PR, we may facilitate anyone who does wish to develop mathlib4 in that direction.

See also the discussion about naming here

For completeness we also introduce the dual Lower Set topology.

ADedecker · 2023-07-11T12:14:48Z

Could you add comments (I'd say both in the module docstrings and in the docs of the definitions) warning that this is not the dual of the LowerTopology? Maybe even add an example in the module docstring.

Mathlib/Topology/Order/UpperSetTopology.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

ghost · 2023-07-31T23:19:31Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Topology/Order/LowerUpperTopology): Dual the lower topology #5873~~
~~[Merged by Bors] - feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff #6157~~
By Dependent Issues (🤖). Happy coding!

ADedecker

Final set of nitpicks.

Thanks!
bors d+

Mathlib/Topology/Order/UpperLowerSetTopology.lean

bors · 2023-08-01T12:15:44Z

✌️ 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: Anatole Dedecker <anatolededecker@gmail.com>

mans0954 · 2023-08-01T18:11:22Z

bors r+

…or Alexandrov) topology and the Lower Set topology (#5672) Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

bors · 2023-08-01T18:35:15Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

…or Alexandrov) topology and the Lower Set topology (#5672) Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

…ff (#6157) Add if and only if versions of `Monotone.dual` and `Antitone.dual`. Needed for #5672 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>

…or Alexandrov) topology and the Lower Set topology (#5672) Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

…ff (#6157) Add if and only if versions of `Monotone.dual` and `Antitone.dual`. Needed for #5672 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>

…or Alexandrov) topology and the Lower Set topology (#5672) Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology. Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

mans0954 and others added 15 commits June 12, 2023 19:23

Introduce Upper Set topology

d66ceb4

Prove something

8fa1fcd

Prove more stuff

cc4eecd

Note conjecture

ccfc6d9

Prove Monotone_iff_Continuous

d612756

Convert to TFAE

7e4d0f9

Complete TFAE

251a6cc

Simplify

bf272c2

Don't need [t,t]

222dd95

Sync with mans0954/scott-topology

ff51ef0

Merge branch 'master' into mans0954/upper-set-topology

9aaf937

Expand motivation

9ea2ace

Add toUpperSetOrderIso

15fe595

Alexandrov property

dbee995

Expand docs

c05afc2

mans0954 mentioned this pull request Jul 2, 2023

[Merged by Bors] - feat: Scott topology on a preorder #2508

Closed

3 tasks

mans0954 added the awaiting-review label Jul 2, 2023

mans0954 added 2 commits July 6, 2023 07:50

Merge branch 'master' into mans0954/upper-set-topology

4fdfd33

Lint

84088df

kim-em added the new-feature label Jul 7, 2023

ADedecker self-assigned this Jul 10, 2023

ADedecker reviewed Jul 11, 2023

View reviewed changes

ADedecker added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 11, 2023

mans0954 and others added 5 commits July 11, 2023 18:00

Update Mathlib/Topology/Order/UpperSetTopology.lean

9ef6ca3

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperSetTopology.lean

876c8d9

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperSetTopology.lean

8f48ca3

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperSetTopology.lean

6f5eaf7

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Explain the relationship between UpperSetTopology and LowerTopology

4d5e9d7

ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jul 31, 2023

mans0954 added 2 commits August 1, 2023 06:09

Merge branch 'master' into mans0954/upper-set-topology

87d15f2

Fix

873ee77

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 1, 2023

ADedecker reviewed Aug 1, 2023

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 1, 2023

mans0954 and others added 7 commits August 1, 2023 18:18

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

c65f6ec

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

81da5cf

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

c8fbede

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

635c020

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

f83c78f

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Update Mathlib/Topology/Order/UpperLowerSetTopology.lean

b9c083c

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Shorten

a4b01e7

bors bot closed this Aug 1, 2023

bors bot deleted the mans0954/upper-set-topology branch August 1, 2023 18:35

ADedecker mentioned this pull request Aug 13, 2023

[Merged by Bors] - fix(Topology/Order/UpperLowerSetTopology): Fix theorem names in UpperLowerSetTopology to match mathlib4 conventions #6557

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Topology/Order/UpperLowerSetTopology): Introduce the Upper Set (or Alexandrov) topology and the Lower Set topology#5672

[Merged by Bors] - feat(Topology/Order/UpperLowerSetTopology): Introduce the Upper Set (or Alexandrov) topology and the Lower Set topology#5672
mans0954 wants to merge 75 commits intomasterfrom
mans0954/upper-set-topology

mans0954 commented Jul 2, 2023 •

edited by github-actions bot

Loading

Uh oh!

ADedecker commented Jul 11, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ghost commented Jul 31, 2023

Uh oh!

ADedecker left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bors bot commented Aug 1, 2023

Uh oh!

mans0954 commented Aug 1, 2023

Uh oh!

bors bot commented Aug 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mans0954 commented Jul 2, 2023 • edited by github-actions bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ADedecker commented Jul 11, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ghost commented Jul 31, 2023

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bors bot commented Aug 1, 2023

Uh oh!

mans0954 commented Aug 1, 2023

Uh oh!

bors bot commented Aug 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mans0954 commented Jul 2, 2023 •

edited by github-actions bot

Loading