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