Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(Topology): clopen subsets of products of compact spaces are unions of clopen boxes #8678

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat(Topology): clopen subsets of products of compact spaces are unions of clopen boxes #8678

wants to merge 22 commits into from

Conversation

dagurtomas
Copy link
Collaborator

Open in Gitpod

@dagurtomas dagurtomas added awaiting-author A reviewer has asked the author a question or requested changes WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 28, 2023
github-actions[bot]
github-actions bot reviewed Nov 28, 2023
View reviewed changes
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
dagurtomas and others added 4 commits November 28, 2023 21:48
@dagurtomas @github-actions
Update docs/references.bib
7b63784 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@dagurtomas @github-actions
Update docs/references.bib
fdd89e3 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@dagurtomas @github-actions
Update docs/references.bib
8198f00 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@dagurtomas @github-actions
Update docs/references.bib
27aafa0 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
github-actions[bot]
github-actions bot reviewed Nov 28, 2023
View reviewed changes
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
github-actions[bot]
github-actions bot reviewed Nov 28, 2023
View reviewed changes
docs/references.bib Outdated Show resolved Hide resolved
docs/references.bib Outdated Show resolved Hide resolved
@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters and removed WIP Work in progress labels Nov 29, 2023
This was referenced Nov 29, 2023
Closed
Closed
jcommelin
jcommelin reviewed Dec 4, 2023
View reviewed changes
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 4, 2023
dagurtomas and others added 3 commits December 4, 2023 22:09
@dagurtomas @jcommelin
Update Mathlib/Topology/ClopenBox.lean
a8b712b 
Co-authored-by: Johan Commelin <johan@commelin.net>
@dagurtomas @jcommelin
Update Mathlib/Topology/ClopenBox.lean
bb09727 
Co-authored-by: Johan Commelin <johan@commelin.net>
@dagurtomas
golf
62c54c8
@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 4, 2023
jcommelin
jcommelin reviewed Dec 5, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

The big proof is pretty big... are there natural sublemmas that can be extracted?

Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
Mathlib/Topology/ClopenBox.lean Outdated Show resolved Hide resolved
@dagurtomas
Copy link
Collaborator Author

I extracted the fact that U is open as a sublemma

@urkud
Copy link
Member

urkud commented Dec 16, 2023

I'm going to golf some proofs now.

@urkud
Copy link
Member

urkud commented Dec 17, 2023

I golfed the proofs using some lemmas that were already in the library. Now we need a review from another maintainer (e.g., I'm not sure if the names I use are too verbose).

@dagurtomas
Copy link
Collaborator Author

These changes look great. Thanks @urkud!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 26, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 29, 2023
@urkud
Copy link
Member

urkud commented Dec 29, 2023

LGTM but I contributed too much to merge it.
maintainer merge

@github-actions GitHub Actions
Copy link

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

jcommelin
jcommelin approved these changes Dec 29, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Dec 29, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 29, 2023
@dagurtomas @urkud
feat(Topology): clopen subsets of products of compact spaces are unio…
b8c9740 
…ns of clopen boxes (#8678)






Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 29, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology): clopen subsets of products of compact spaces are unions of clopen boxes [Merged by Bors] - feat(Topology): clopen subsets of products of compact spaces are unions of clopen boxes Dec 29, 2023
@mathlib-bors mathlib-bors bot closed this Dec 29, 2023
@mathlib-bors mathlib-bors bot deleted the dagur_ClopenBox branch December 29, 2023 08:24
This was referenced Jan 7, 2024
Closed
Closed
@dagurtomas dagurtomas mentioned this pull request Mar 22, 2024
Closed
7 tasks
mathlib-bors bot pushed a commit that referenced this pull request May 14, 2024
@dagurtomas
feat(Condensed): light condensed objects (#11586)
5602b56 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
callesonne pushed a commit that referenced this pull request May 16, 2024
@dagurtomas @callesonne
feat(Condensed): light condensed objects (#11586)
5972017 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
grunweg pushed a commit that referenced this pull request May 17, 2024
@dagurtomas @grunweg
feat(Condensed): light condensed objects (#11586)
c697b59 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
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

@github-actions github-actions[bot] github-actions left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. 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.

None yet
4 participants
@dagurtomas @urkud @jcommelin @leanprover-community-mathlib4-bot