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 α]!

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.

I've asked on zulip.

awaiting-author

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

@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.)

awaiting-review

bors merge

Thanks for the quick reviews, this time!

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported