## Stream: maths

### Topic: topology

#### Reid Barton (Dec 13 2018 at 22:39):

Hi @Sebastien Gouezel, I was wondering whether you either have proved or were planning to prove Urysohn'slemma or the Tietze extension theorem.
I ask because I have an ugly, but working proof of the former lying around somewhere, and part of a proof of the latter, and it looks like your PR #464 is the main thing I would need to finish it off.

#### Sebastien Gouezel (Dec 14 2018 at 07:13):

No, I have not done it, and I don't plan to do it. You can go ahead if you want!

#### Reid Barton (Oct 07 2019 at 15:03):

So I started trying to write module documentation for topology but (perhaps predictably) I ended up doing another reorganization--hopefully less drastic than the one from March. It is still in progress, but I will be posting a few preliminary PRs.

Great!

#### Reid Barton (Oct 07 2019 at 16:46):

Currently, topology.constructions is a big grab-bag which I found difficult to document. For example, it doesn't actually contain any constructions themselves, but rather theorems about them, but sometimes those theorems are somewhere else.
So here's what I'm trying.

• Move the definitions of product topology, etc. from near the end of topology.order to a new file (working name: topology.basic_constructions) which imports topology.order. Also move the most elementary facts about these constructions there (e.g., projections are continuous).
• Import topology.basic_constructions in most other modules, in order to move proofs like "if $S \subset X$ and $T \subset Y$ are compact, then $S \times T$ is compact" to near the definition of compactness.
• A few basic facts about products and so on (like is_open_prod_iff') use concepts (like is_open_map) which are defined in later files, so those will remain in topology.constructions (which should perhaps be renamed), which will end up a hopefully much smaller grab-bag.

#### Reid Barton (Oct 07 2019 at 16:46):

So far I implemented this for prod and not any of the other constructions, but it appears to be going well.

#### Reid Barton (Oct 07 2019 at 16:47):

@Patrick Massot, you likely tried something like this in the original refactoring; do you see any particular snags?

#### Reid Barton (Oct 07 2019 at 16:59):

I'm really tempted to rename all the space variables to X Y Z W first...

#### Reid Barton (Oct 07 2019 at 17:00):

since it will make this refactoring a lot easier

Go for it!

#### Patrick Massot (Oct 07 2019 at 17:25):

Reid, please feel free to reorganize things. I got tired during the previous refactor, and Johannes was pushing towards big files. But the current situation is far from perfect.

#### Johan Commelin (Oct 07 2019 at 18:22):

@Reid Barton One thing I wondered is whether embedding and dense_embedding etc should use old_structure_cmd.

#### Reid Barton (Oct 07 2019 at 18:23):

but I'm trying to leave such changes for separate PRs

fair enough

#### Reid Barton (Oct 07 2019 at 18:28):

At the moment I'm just trying to get the right stuff total in each file, then after that each file can be fixed up nicely

#### Patrick Massot (Oct 07 2019 at 20:51):

@Reid Barton while your are refactoring topology, it would be nice to use the new localized notation feature. I think nhds deserves a notation. In the perfectoid project I always use local notation 𝓝 x:70 := nhds x

#### Patrick Massot (Oct 07 2019 at 20:52):

In top of the eye candy, the precedence allows to avoid many parentheses.

#### Reid Barton (Oct 12 2019 at 14:55):

This refactoring is now #1541.

#### Reid Barton (Oct 12 2019 at 15:05):

I ended up doing slightly less reordering of imports than planned, and pretty much every theorem ended up in a logical file, though possibly the ordering of imports is "overfit" to the particular set of theorems we have currently.

#### Patrick Massot (Oct 12 2019 at 15:21):

@Reid Barton did you run sanity_check on all those files?

#### Patrick Massot (Oct 12 2019 at 15:22):

Also, your new README is wonderful, but it should go to https://github.com/leanprover-community/mathlib/tree/master/docs/theories

#### Reid Barton (Oct 12 2019 at 15:22):

It's running currently

I think

#### Mario Carneiro (Oct 12 2019 at 15:22):

is sanity_check in travis?

#### Patrick Massot (Oct 12 2019 at 15:23):

Honestly, if such a PR builds and sanity_checks (and makes sense from a general point of view) then I don't see what I should review. Of course the next step is to make sure every file has a toplevel docstring and doc_blame, but that can be done later (super fast merging is crucial to such PRs).

#### Reid Barton (Oct 12 2019 at 15:24):

I'm also going to go through the same process I did for the linear algebra renaming PR to check that I didn't mess up any declarations

Oh I see

#### Patrick Massot (Oct 12 2019 at 15:25):

After a couple of uses like this, sharpening your tool, it would be nice to make it available.

Good idea, done

#### Reid Barton (Oct 12 2019 at 15:37):

Reid Barton did you run sanity_check on all those files?

sanity_check found a mistake in my #1516, but not this one. I'll fix it in an independent PR.

#### Reid Barton (Oct 12 2019 at 18:34):

(moving back here) I guess we can merge aside from the question about the README.md.
I thought of the file as saying "if you want to find X, look in file Y", rather than trying to list everything that exists in topology, although I guess it also accomplishes that as a side effect.

#### Patrick Massot (Oct 12 2019 at 18:35):

My point is we don't have any other files like that in that place.

#### Reid Barton (Oct 12 2019 at 18:35):

It's true--I think it would be nice if we did; but maybe this PR isn't the place to make that argument?

#### Reid Barton (Oct 12 2019 at 18:36):

What's the alternative? I guess I could append the contents of README.md to the end of docs/theories/topological_spaces.md, under a heading like "File organization"

#### Patrick Massot (Oct 12 2019 at 18:37):

Yes, maybe after renaming it to topology.md

#### Reid Barton (Oct 12 2019 at 18:38):

These docs are just concerned with the contents of the topological_space.lean file.

which no longer exists

#### Reid Barton (Oct 12 2019 at 19:02):

Okay, I've done this (for now, at least)

oops hang on

#### Reid Barton (Oct 12 2019 at 19:04):

okay, it should be correct now

Last updated: May 10 2021 at 06:13 UTC