Skip to content

[Merged by Bors] - feat: Topological properties of order-connected sets in ℝⁿ#10565

Closed
YaelDillies wants to merge 4 commits intomasterfrom
YK-Yael-normed-order
Closed

[Merged by Bors] - feat: Topological properties of order-connected sets in ℝⁿ#10565
YaelDillies wants to merge 4 commits intomasterfrom
YK-Yael-normed-order

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 14, 2024 •
edited by github-actions bot
Loading

@YaelDillies YaelDillies added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged t-analysis Analysis (normed *, calculus) t-order Order theory labels Feb 14, 2024
@urkud urkud self-assigned this Feb 14, 2024
urkud
urkud reviewed Feb 15, 2024
View reviewed changes
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 15, 2024
@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 15, 2024
urkud
urkud reviewed Feb 19, 2024
View reviewed changes
urkud
urkud reviewed Feb 19, 2024
View reviewed changes
urkud
urkud reviewed Feb 19, 2024
View reviewed changes
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 19, 2024
@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 19, 2024
@ghost 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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 21, 2024
@YaelDillies YaelDillies requested a review from urkud March 2, 2024 12:43
@ghost 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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 8, 2024
@ghost 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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 17, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Mar 17, 2024
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 23, 2024
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 23, 2024
View reviewed changes
@YaelDillies YaelDillies added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 23, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 23, 2024
@ghost
Copy link
Copy Markdown

ghost commented Mar 23, 2024

This PR/issue depends on:

Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 7, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Seems pretty straightforward, modulo the removal of Topology.Order.Bounded

@YaelDillies YaelDillies force-pushed the YK-Yael-normed-order branch from 08e3933 to cf1e03a Compare June 7, 2024 08:34
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

Dependency changes
File Base Count Head Count Change
Mathlib.Analysis.Normed.Order.UpperLower 1150 1153 +3 (+0.26%)

Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 7, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 7, 2024
fpvandoorn
fpvandoorn reviewed Jun 7, 2024
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.

One more comment. Feel free to merge even if you disagree.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 7, 2024

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 7, 2024
j-loreaux
j-loreaux reviewed Jun 7, 2024
View reviewed changes
Mathlib/Analysis/Normed/Order/UpperLower.lean
Comment on lines +28 to +31
Is there a way to generalise `IsClosed.upperClosure_pi`/`IsClosed.lowerClosure_pi` so that they also
apply to `ℝ`, `ℝ × ℝ`, `EuclideanSpace ι ℝ`? `_pi` has been appended to their names to disambiguate
from the other possible lemmas, but we will want there to be a single set of lemmas for all
situations.
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux Jun 7, 2024

Choose a reason for hiding this comment

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

This comment shouldn't hold up this PR, but the relevant lemmas could just take a homeomorphism with a pi-type as an explicit argument. It's not a pretty solution, but I think it would work, and I believe we already have the necessary homeomorphisms available.

(On second thought, would it need to be an order isomorphism too? That probably rules out this idea as being useful)

Copy link
Copy Markdown
Contributor Author

@YaelDillies YaelDillies Jun 7, 2024

Choose a reason for hiding this comment

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

Yeah, it would also need to be an order isomorphism. That's the crux. We need a way to say "Order on this type is given by those coordinates", which sounds a lot like the Inducing/Embedding business in the topology part of the library.

Food for thought, I guess

@YaelDillies YaelDillies removed the request for review from urkud June 7, 2024 18:08
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 7, 2024

bors merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

PR summary

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Analysis.Normed.Order.UpperLower 1150 1153 +3 (+0.26%)

Diff of declarations

+ BddAbove.isBounded
+ BddAbove.isBounded_inter
+ BddBelow.isBounded
+ BddBelow.isBounded_inter
+ Bornology.IsBounded.bddAbove
+ Bornology.IsBounded.bddBelow
+ Bornology.IsBounded.subset_Icc_sInf_sSup
+ IsClopen.lowerClosure_pi
+ IsClopen.upperClosure_pi
+ IsClosed.lowerClosure_pi
+ IsClosed.upperClosure_pi
+ IsOrderBornology
+ OrderDual.instIsOrderBornology
+ Pi.instIsOrderBornology
+ Prod.instIsOrderBornology
+ _root_.BddAbove.isBoundedUnder
+ _root_.BddBelow.isBoundedUnder
+ bddAbove_preimage_ofDual
+ bddAbove_preimage_toDual
+ bddBelow_preimage_ofDual
+ bddBelow_preimage_toDual
+ closure_lowerClosure_comm_pi
+ closure_upperClosure_comm_pi
+ dist_anti_left_pi
+ dist_anti_right_pi
+ dist_inf_sup_pi
+ dist_le_dist_of_le_pi
+ dist_mono_left_pi
+ dist_mono_right_pi
+ instBornology
+ instIsOrderBornology
+ isBounded_iff_bddBelow_bddAbove
+ isBounded_preimage_ofDual
+ isBounded_preimage_toDual
+ isCobounded_preimage_ofDual
+ isCobounded_preimage_toDual
+ isOrderBornology_iff_eq_orderBornology
+ lowerClosure_interior_subset'
+ orderBornology
+ orderBornology_isBounded
+ upperClosure_interior_subset'
- Real.isBounded_iff_bddBelow_bddAbove
- Real.subset_Icc_sInf_sSup_of_isBounded

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 7, 2024

Canceled.

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 7, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 7, 2024
@YaelDillies
feat: Topological properties of order-connected sets in ℝⁿ (#10565)
00f01c9 
Partially forward-port leanprover-community/mathlib3#16976
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 7, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 7, 2024
@YaelDillies
feat: Topological properties of order-connected sets in ℝⁿ (#10565)
cde4ac6 
Partially forward-port leanprover-community/mathlib3#16976
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 7, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 7, 2024
@YaelDillies
feat: Topological properties of order-connected sets in ℝⁿ (#10565)
3ee149a 
Partially forward-port leanprover-community/mathlib3#16976
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Topological properties of order-connected sets in ℝⁿ [Merged by Bors] - feat: Topological properties of order-connected sets in ℝⁿ Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the YK-Yael-normed-order branch June 8, 2024 00:32
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
feat: Topological properties of order-connected sets in ℝⁿ (#10565)
f798fcb 
Partially forward-port leanprover-community/mathlib3#16976
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

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

@fpvandoorn fpvandoorn fpvandoorn left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

@urkud urkud

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged t-analysis Analysis (normed *, calculus) t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@YaelDillies @urkud @eric-wieser @fpvandoorn @j-loreaux @Ruben-VandeVelde