[Merged by Bors] - chore(Topology/{Compactness/Compact}, Irreducible}): rename type variables

[grunweg]

X, Y, Z are standard mathematical names for topological spaces.
As discussed on zulip, let us rename them.

As a drive-by commit, re-use the declared variables $\iota$, $s$ and $t$ (more) when stating theorems.

---

I'm following by checklist here.

[eric-wieser]

X, Y, Z are standard mathematical names for topological spaces.

I'm not sure if this is true in mathlib; I've seen greek letters in lots of places too. There is only one mention of topology in the style guide, and it uses [DiscreteTopology α]!

[grunweg]

X, Y, Z are standard mathematical names for topological spaces.

I'm not sure if this is true in mathlib; I've seen greek letters in lots of places too. There is only one mention of topology in the style guide, and it uses [DiscreteTopology α]!

I agree that Greek letters are pervasive in topology files. In math textbooks, I've always seen X, Y, Z etc., though. Hence, my guess was that general topology files, being old enough, were written when Greek letter prevailed. (It's possible I'm wrong, though!)

As a case in point, I've looked at the first ten files in the Topology root folder: two use names X, Y, Z, the others use Greek letters --- but almost all of the latter have copyright years 2019 or earlier.

[grunweg]

I've asked on zulip.

[grunweg]

awaiting-author

[PatrickMassot]

I'm sorry we haven't been quick enough to merge that one. Could you please try to fix the conflicts?

[grunweg]

@PatrickMassot Updated; as soon as this passes CI, it should be ready for review.
The merge meant I had to basically re-do these changes; it might be easier to just review/skim all commits since the merge separately. (They're logically independent.)

[grunweg]

awaiting-review

[PatrickMassot]

bors merge

[grunweg]

Thanks for the quick reviews, this time!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported