Use standard names for topological spaces

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 α.

Search the Topology directory and the rest of mathlib for files containing TopologicalSpace α, then review the checklist in PR #7589's comment. Use the variable declarations and VS Code's rename handler as entry points, checking docstrings and missed occurrences. Done means affected spaces consistently use standard names such as X, Y, and Z.