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(LightProfinite): light profinite sets as sequential limits with surjective transition maps #13333

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - feat(LightProfinite): light profinite sets as sequential limits with surjective transition maps #13333

wants to merge 33 commits into from

Conversation

dagurtomas
Copy link
Collaborator

@dagurtomas dagurtomas commented May 29, 2024 •
edited by github-actions bot
Loading

Adds the file LightProfinite/AsLimit which mirrors Profinite/AsLimit.

Open in Gitpod

dagurtomas and others added 18 commits May 17, 2024 14:23
@dagurtomas
feat(Topology): a profinite space has countably many clopens iff it i…
1747555 
…s second countable
@dagurtomas
golf
4b76e3e
@dagurtomas
Update Compact.lean
13ca0cf
@dagurtomas
Merge branch 'master' into dagur/SecondCountableClopens
6541d50
@dagurtomas
Merge branch 'master' into dagur/SecondCountableClopens
86a2011
@dagurtomas
golf
42e26ad
@dagurtomas @jcommelin
Update Mathlib/Topology/Compactness/Compact.lean
2a24309 
Co-authored-by: Johan Commelin <[email protected]>
@dagurtomas @jcommelin
Update Mathlib/Topology/Compactness/Compact.lean
d3960af 
Co-authored-by: Johan Commelin <[email protected]>
@dagurtomas
fix errors
af3c9a2
@dagurtomas
refactor(LightProfinite): redefine light profinite spaces as second c…
508dace 
…ountable profinite spaces
@dagurtomas
aslimit file
8fa0af9
@dagurtomas
remove file for future PR
31f7ff8
@dagurtomas
mathlib file
e36c047
@dagurtomas
Merge branch 'master' into dagur/LightProfiniteRefactor
94d5bd4
@dagurtomas
lint
e3b89d3
@dagurtomas
feat(LightProfinite): light profinite sets as sequential limits with …
7bfadef 
…surjective transition maps
@dagurtomas
mathlib
b086057
@dagurtomas
move instance
be5333f
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 29, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 30, 2024
@dagurtomas dagurtomas added awaiting-review awaiting-CI t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jun 4, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 11, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@dagurtomas dagurtomas added awaiting-author A reviewer has asked the author a question or requested changes WIP Work in progress and removed awaiting-review labels Jun 11, 2024
@dagurtomas dagurtomas added awaiting-review awaiting-CI and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Jul 2, 2024
@dagurtomas dagurtomas mentioned this pull request Jul 2, 2024
Closed
11 tasks
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 14, 2024
@dagurtomas dagurtomas removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 15, 2024
@dagurtomas dagurtomas requested a review from kim-em July 16, 2024 22:04
@kim-em
Copy link
Contributor

kim-em commented Jul 17, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 17, 2024
@dagurtomas
feat(LightProfinite): light profinite sets as sequential limits with …
540a3ad 
…surjective transition maps (#13333)

Adds the file `LightProfinite/AsLimit` which mirrors `Profinite/AsLimit`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LightProfinite): light profinite sets as sequential limits with surjective transition maps [Merged by Bors] - feat(LightProfinite): light profinite sets as sequential limits with surjective transition maps Jul 17, 2024
@mathlib-bors mathlib-bors bot closed this Jul 17, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/LightProfiniteAsLimit branch July 17, 2024 18:38
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-category-theory Category theory 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.
3 participants
@dagurtomas @leanprover-community-mathlib4-bot @kim-em