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

[Merged by Bors] - feat(analysis/normed/order/upper_lower): Thickening an upper set#17257

Closed
YaelDillies wants to merge 15 commits intomasterfrom
upper_lower_norm
Closed

[Merged by Bors] - feat(analysis/normed/order/upper_lower): Thickening an upper set#17257
YaelDillies wants to merge 15 commits intomasterfrom
upper_lower_norm

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Oct 30, 2022 •
edited
Loading

Results about upper sets in normed ordered groups.

This includes somewhat specific results that will be needed to prove that order-connected sets in ℝⁿ are measurable.

Match leanprover-community/mathlib4#2896

Open in Gitpod

@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-analysis Analysis (normed *, calculus) t-order Order hierarchy labels Oct 30, 2022
@YaelDillies YaelDillies mentioned this pull request Oct 30, 2022
Closed
6 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 Feb 17, 2023
@ghost
Copy link
Copy Markdown

ghost commented Feb 17, 2023

This PR/issue depends on:

YaelDillies
YaelDillies commented Feb 17, 2023
View reviewed changes
src/topology/algebra/order/upper_lower.lean
Comment on lines +18 to +19
The same lemmas are true in the additive/multiplicative worlds. To avoid code duplication, we
provide `has_upper_lower_closure`, an ad hoc axiomatisation of the properties we need.
Copy link
Copy Markdown
Collaborator Author

@YaelDillies YaelDillies Feb 17, 2023

Choose a reason for hiding this comment

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

We just merged a wrong module doc. This is fixing it. Sorry about that.

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Mar 14, 2023

lgtm
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 14, 2023

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

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Mar 14, 2023

It looks like upper_lower has been ported by now, can you forward port your change there too please?

@YaelDillies YaelDillies mentioned this pull request Mar 15, 2023
Closed
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Mar 15, 2023

Done

@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Mar 15, 2023

I'm wondering if we should strong_lt more widely in the library (including here), but that is outside the scope of this PR.

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Mar 15, 2023
@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Mar 15, 2023
bors bot pushed a commit that referenced this pull request Mar 15, 2023
@YaelDillies
feat(analysis/normed/order/upper_lower): Thickening an upper set (#17257
992efbd 
)

Results about upper sets in normed ordered groups.
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Mar 15, 2023

I introduced strong_lt partly for this purpose, but I wasn't sure whether it would obscure the results or not.

@bors
Copy link
Copy Markdown

bors bot commented Mar 15, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed/order/upper_lower): Thickening an upper set [Merged by Bors] - feat(analysis/normed/order/upper_lower): Thickening an upper set Mar 15, 2023
@bors bors bot closed this Mar 15, 2023
@bors bors bot deleted the upper_lower_norm branch March 15, 2023 16:02
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 21, 2023
@YaelDillies @Parcly-Taxel
chore: Fix Topology.Algebra.Order.UpperLower docstring (#2896)
eae4bf3 
Match leanprover-community/mathlib3#17257



Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus) t-order Order hierarchy

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @alexjbest @fpvandoorn