Use standard names for topological spaces

[grunweg]

Currently, many old files (in topology and elsewhere) still use Greek letters for topological spaces. Newer files use e.g. the letters X, Y and Z. We should switch to using these everywhere (per Zulip discussion.

A lot of files have already been converted, but there is still a fair number to go.

Which files are affected? As an approximation, search for files containing the string TopologicalSpace α. As of January 20th, 2024, there are 95 such files in Topology alone (of which 3 have open PRs), and 145 files in all of mathlib.

How to replace? What to look out for?

• I compiled a checklist here.
• VS Code's rename handler is useful for renaming variables: go to the declaration site (e.g. a variable statement mentioning something like {α : Type*} or {α : Type u}, select the variable name and press F2. Sometimes, that doesn't catch all occurrences and you need to rename again. You'll also need to check if docstrings mention α.

[YaelDillies]

I think using α makes a lot of sense to mean an unspecified topological space.