Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(topology/algebra/order/upper_lower): The closure of an upper set#16975

Closed
YaelDillies wants to merge 23 commits intomasterfrom
upper_lower_topology
Closed

[Merged by Bors] - feat(topology/algebra/order/upper_lower): The closure of an upper set#16975
YaelDillies wants to merge 23 commits intomasterfrom
upper_lower_topology

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Oct 14, 2022 •
edited
Loading

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 14, 2022
@YaelDillies YaelDillies mentioned this pull request Oct 14, 2022
Closed
6 tasks
@YaelDillies YaelDillies mentioned this pull request Oct 23, 2022
Closed
1 task
@YaelDillies YaelDillies mentioned this pull request Oct 30, 2022
Closed
7 tasks
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 31, 2022
urkud
urkud reviewed Nov 5, 2022
View reviewed changes
YaelDillies
YaelDillies commented Nov 5, 2022
View reviewed changes
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 6, 2022
@YaelDillies YaelDillies mentioned this pull request Nov 6, 2022
Closed
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 7, 2022
@ghost
Copy link
Copy Markdown

ghost commented Nov 7, 2022

This PR/issue depends on:

@YaelDillies YaelDillies mentioned this pull request Nov 8, 2022
Closed
eric-wieser
eric-wieser reviewed Nov 26, 2022
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 11, 2022
View reviewed changes
kex-y
kex-y reviewed Feb 11, 2023
View reviewed changes
@YaelDillies @kex-y
typo
19b6bb1 
Co-authored-by: Kexing Ying <kexing.ying19@imperial.ac.uk>
@kex-y
Copy link
Copy Markdown
Member

kex-y commented Feb 12, 2023

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 12, 2023

🚀 Pull request has been placed on the maintainer queue by JasonKYi.

fpvandoorn
fpvandoorn approved these changes Feb 16, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

Presumably there is also an instance "linear order + order closed -> has_upper_lower_closure"?

Don't forget the mathlib4 PR for the single-line change in group_action/opposite.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Feb 16, 2023

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

@leanprover-community-bot-assistant 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 Feb 16, 2023
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Feb 16, 2023

I did not manage to prove the instance you're thinking of. I suspect it's just not true, because all you can say about upper_closure s is that it's ⋃ a ∈ s, Ici a, which is not obviously open (when you have an ordered_comm_group, you can rewrite that as a union of translates of s, which then has to be open).

bors merge

bors bot pushed a commit that referenced this pull request Feb 16, 2023
@YaelDillies
feat(topology/algebra/order/upper_lower): The closure of an upper set (…
4330aae 
…#16975)

Topological facts about order-connected sets.
@bors
Copy link
Copy Markdown

bors bot commented Feb 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/algebra/order/upper_lower): The closure of an upper set [Merged by Bors] - feat(topology/algebra/order/upper_lower): The closure of an upper set Feb 17, 2023
@bors bors bot closed this Feb 17, 2023
@bors bors bot deleted the upper_lower_topology branch February 17, 2023 00:41
@YaelDillies YaelDillies mentioned this pull request Feb 17, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 17, 2023
@YaelDillies
chore: Missing to_additive on CommSemigroup.isCentralScalar (#2344)
1391918 
Match leanprover-community/mathlib3#16975
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 1, 2023
@YaelDillies @eric-wieser @fpvandoorn
chore: Missing to_additive on CommSemigroup.isCentralScalar (#2344)
90bb14f 
The SHA was already updated in #2498, but the `#align` was forgotten, and the instance name was incorrectly generated.

Match leanprover-community/mathlib3#16975.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

4 more reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@kex-y kex-y kex-y left review comments

@fpvandoorn fpvandoorn fpvandoorn approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@YaelDillies @kex-y @urkud @eric-wieser @fpvandoorn @leanprover-community-bot-assistant