[Merged by Bors] - chore(Topology/SubsetProperties): Refactor SubsetProperties.lean#7628
[Merged by Bors] - chore(Topology/SubsetProperties): Refactor SubsetProperties.lean#7628
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
@loefflerd was the reviewdog misbehaving here? Or being not as helpful as it could be somehow, I'd like to improve it if so but the history is now very confusing |
There was a problem hiding this comment.
I have carefully checked over this (admittedly by hand) and I can attest that the following summary is accurate:
- The file
Mathlib.Topology.SubsetPropertieshas been renamed toMathlib.Topology.Compactness.Compactas well as having its length cut from about 2k lines to about 1k lines. - The c.1k lines removed from
Mathlib.Topology.SubsetPropertiesexactly correspond to the content added in the four new filesTopology.Clopen,Topology.Irreducible,Topology.Compactness.LocallyCompact,Topology.Compactness.SigmaCompact. Indeed there is a character-by-character match except for file headers and four locations (occuring in the new fileTopology.irreducible) whereα : Type uwas changed toα : Type*. - The file
Topology.Paracompactwas renamed toTopology.Compactness.Paracompact - Two results (
isClosed_and_discrete_iffandFilter.codiscrete) were moved out ofMathlib.Topology.SubsetPropertiesand placed inTopology.DiscreteSubset. - File headers were added / updated according to the changes, in some cases by migrating comments from
Mathlib.Topology.SubsetProperties(e.g., remarks aboutIsPreirreducible). - All other files changed have only had their
importstatements fixed to handle the new file layout.
Thanks for doing this.
bors d+
Mathlib/Topology/DiscreteSubset.lean
Outdated
|
|
||
| /-- Criterion for a subset `S ⊆ α` to be closed and discrete in terms of the punctured | ||
| neighbourhood filter at an arbitrary point of `α`. (Compare `discreteTopology_subtype_iff`.) -/ | ||
| theorem isClosed_and_discrete_iff {α : Type*} [TopologicalSpace α] {S : Set α} : |
There was a problem hiding this comment.
I recognise that when splitting a large file it is best to keep any ancillary changes to an absolute minimum but perhaps here we could make an exception and use carrier types that are consistent with the cofinite_cocompact above
| theorem isClosed_and_discrete_iff {α : Type*} [TopologicalSpace α] {S : Set α} : | |
| theorem isClosed_and_discrete_iff {X : Type*} [TopologicalSpace X] {S : Set X} : |
(likewise in Filter.codiscrete below)
|
✌️ loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
|
bors r+ |
|
Thanks a lot @loefflerd! This is very tedious work that is very useful. |
Split up the 2000-line `Topology/SubsetProperties.lean` into several smaller files. Not only is it too huge, but the name is very unhelpful, since actually about 90% of the file is about compactness; I've moved this material into various files inside a new subdirectory `Topology/Compactness/`.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Was introduced in #7628.
Split up the 2000-line
Topology/SubsetProperties.leaninto several smaller files. Not only is it too huge, but the name is very unhelpful, since actually about 90% of the file is about compactness; I've moved this material into various files inside a new subdirectoryTopology/Compactness/.