Hereditarily paracompact (P216), ordinal (P190) spaces are countable (P57)

[felixpernegger]

No description provided.

[prabau]

@felixpernegger Sorry, one more thing one should pay attention to when doing the merge.
If there is only one commit in the PR, github seems to take the title of that commit as the title of the "squashed commit" for squash and merge into main. So the commit in main ended up being:

commit 70c9de88466fe4995606544bb9909c5293649bc0
Author: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Sat Dec 27 09:34:56 2025 +0100

finish (#1557)
which is very uninformative.

So general rule: when working on a PR, the first commit should have a good title that summarizes the work being done.

And if for some reason this was not the case, one can manually modify the title of the squashed commit when doing the squash and merge.

(@Moniker1998 @yhx-12243 fyi)