Skip to content

[Merged by Bors] - feat(LightProfinite): define ℕ∪{∞} as a light profinite set#13358

Closed
dagurtomas wants to merge 31 commits intomasterfrom
dagur/OnePointN
Closed

[Merged by Bors] - feat(LightProfinite): define ℕ∪{∞} as a light profinite set#13358
dagurtomas wants to merge 31 commits intomasterfrom
dagur/OnePointN

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented May 29, 2024 •
edited
Loading

dagurtomas and others added 19 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 <johan@commelin.net>
@dagurtomas @jcommelin
Update Mathlib/Topology/Compactness/Compact.lean
d3960af 
Co-authored-by: Johan Commelin <johan@commelin.net>
@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(Topology): some lemmas about continuity of functions out of one …
877b624 
…point compactifications
@dagurtomas
golf
57b46fc
@dagurtomas
Merge branch 'dagur/LightProfiniteRefactor' into dagur/OnePointN
fd70848
@dagurtomas
feat(LightProfinite): define N union infinity as a light profinite set
5e88acf
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 29, 2024
github-actions[bot]
github-actions bot reviewed May 29, 2024
View reviewed changes
@ghost ghost 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-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jun 4, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 4, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 4, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 11, 2024 •
edited
Loading

PR summary 48a8c845a4

Import changes

No significant changes to the import graph

Declarations diff

+ closedEmbedding_natUnionInftyEmbedding
+ continuous_iff_convergent
+ instance (X : Type*) [TopologicalSpace X] [c : CompactSpace X] [MetrizableSpace X] :
+ instance : Coe ℕ ℕ∪{∞} := optionCoe
+ instance : MetrizableSpace (OnePoint ℕ) := closedEmbedding_natUnionInftyEmbedding.metrizableSpace
+ natUnionInftyEmbedding

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>

@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 16, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 16, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 16, 2024
@dagurtomas dagurtomas added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 17, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 17, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 17, 2024
@dagurtomas dagurtomas mentioned this pull request Jul 10, 2024
Closed
3 tasks
jcommelin
jcommelin reviewed Jul 12, 2024
View reviewed changes
Copy link
Copy Markdown
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

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@dagurtomas
feat(LightProfinite): define ℕ∪{∞} as a light profinite set (#13358)
31c0e2a 
- [x] depends on: #13319 
- [x] depends on: #13355
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LightProfinite): define ℕ∪{∞} as a light profinite set [Merged by Bors] - feat(LightProfinite): define ℕ∪{∞} as a light profinite set Jul 12, 2024
@mathlib-bors mathlib-bors bot closed this Jul 12, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/OnePointN branch July 12, 2024 14:35
@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

@jcommelin jcommelin jcommelin left review comments

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

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 @jcommelin @kim-em