# Zulip Chat Archive

## Stream: maths

### Topic: Splitting topology

#### Patrick Massot (Jan 22 2019 at 13:59):

@Mario Carneiro @Johannes Hölzl @Reid Barton I continued moving on the topology reorganization project. The next step was to split `topology.basic`

and `topology.continuity`

while gathering the basics of continuity and the basics of topological spaces. My current result is at https://github.com/leanprover-community/mathlib/tree/top_split I need comments before moving on. My next step would be to reorganize uniform spaces and topological structures, still following the general scheme discussed in Amsterdam

#### Patrick Massot (Jan 22 2019 at 14:07):

Recall that one goal was to have files with less than 1000 lines, and lighters dependencies for stuff needing only the basics of topological spaces and continuous functions. The current lines counts are

1927 basic.lean 460 bounded_continuous_function.lean 118 compact_open.lean 1568 continuity.lean 271 stone_cech.lean

my proposal has:

206 bases.lean 591 basic.lean 460 bounded_continuous_function.lean 118 compact_open.lean 957 constructions.lean 359 maps.lean 132 opens.lean 573 order.lean 280 separation.lean 272 stone_cech.lean 468 subset_properties.lean

you can still see I got tired with `constructions.lean`

(which has products, sum, quotients, pi...). That one could probably be split more

#### Patrick Massot (Jan 22 2019 at 14:10):

Damn, I forgot to move homeomorphisms from constructions to map

#### Patrick Massot (Jan 22 2019 at 14:11):

That will improve the balance for about 100 lines

#### Johannes Hölzl (Jan 22 2019 at 14:13):

Hm the homeomorphisms should be in `basic`

. And I should mention that I don't like to goal of keeping the files less than 1000 lines. This is quiet arbitrary and doesn't tell anybody where to find a specific definition/proof

#### Johannes Hölzl (Jan 22 2019 at 14:13):

But looking through the changeset it looks very sensible

#### Patrick Massot (Jan 22 2019 at 14:20):

We know you don't like reducing line counts. This was very clear from reading the topology part of mathlib, and also from the Amsterdam discussion. But I think this is still a nice goal, especially when we find out there are sensible cutting points. And of course the 1000 number is totally arbitrary, although there is a certain psychological impact above that threshold.

#### Patrick Massot (Jan 22 2019 at 22:03):

So, should I open a PR?

#### Johannes Hölzl (Jan 22 2019 at 22:23):

Yes, I think this is a good PR

#### Reid Barton (Jan 23 2019 at 14:11):

I made this little ASCII art diagram of the proposed import structure (hopefully I caught everything):

basic------------------- | | order--------- subset_properties | | | separation bases | | | | | maps | opens | | | | constructions-----------

#### Patrick Massot (Jan 23 2019 at 16:13):

This is probably correct. The fact that `constructions`

uses (almost) everything else is probably proving that it was not split enough. There are other files in this directory that import `constructions`

#### Patrick Massot (Jan 23 2019 at 16:14):

Reid, do you want to work some more on this effort?

Last updated: May 12 2021 at 07:17 UTC