Hereditarily realcompact (P215), ordinal (P190) spaces are countable (P57)

[felixpernegger]

No description provided.

[felixpernegger]

@felixpernegger did you look at how I modified your post?

Wrong PR, but looks good!

[Moniker1998]

Yeah I only realized I'm looking at the wrong thing after.
@felixpernegger by the way it's good opportunity for you to squash and merge. Like we discussed before delete the extended description part.

[felixpernegger]

Yeah I only realized I'm looking at the wrong thing after. @felixpernegger by the way it's good opportunity for you to squash and merge. Like we discussed before delete the extended description part.

Isnt it already deleted? Just wanna make sure

[Moniker1998]

@felixpernegger it might not be there. Either way

[prabau]

@felixpernegger FYI, you can check the result of the merge by doing git log on the command line, from the main branch.
For the first commit where you did the merge, you will see a lot of unnecessary cruft, that we don't want to see:

Compare the first commit with the later commits. The first commit has the details of all the little commits that went into the PR, including "finish, typo, updating a particular file, etc. For some other PRs in the past, for people who did not know how to merge properly, we even had dozens of these little changes. This is completely ridiculous. We don't want to see any of that. All the matters is the final result. That's why we follow the "squash and merge" method when doing the final merge of a PR into the main branch. I.e., all the little commits of the PR get squashed into a single commit, and then that commit gets merged into main. But we don't want to see all these little intermediate steps. It just clutters everything.
And note that if anyone is interested in seeing the details of all that, they can still see all of it by going to the github page for that PR.

Practically, when doing a squash and merge, before clicking on the "squash and merge" button, you must blank out the description and only keep the title. See #1185 (comment) and the links there.

Does that make sense?

[prabau]

@felixpernegger @Moniker1998 @yhx-12243 One other thing. You added the theorem
[ ordinal + hereditarily realcompact => countable ].

The title of the PR mentions another theorem
[ ordinal + hereditarily paracompact => countable ],
which is also true, but is not deducible from other results in pi-base.

Any reason why we don't want to add that one?

[yhx-12243]

Casually saying, ordinal + hereditarily paracompact “almost” implies ordinal + hereditarily realcompact, but it has a gap of cardinality < every measurable cardinal

[prabau]

Exactly. The proof without the measurable cardinal condition is basically the same as T810 that was added in this PR. Very easy.

[felixpernegger]

@felixpernegger FYI, you can check the result of the merge by doing git log on the command line, from the main branch. For the first commit where you did the merge, you will see a lot of unnecessary cruft, that we don't want to see:

Compare the first commit with the later commits. The first commit has the details of all the little commits that went into the PR, including "finish, typo, updating a particular file, etc. For some other PRs in the past, for people who did not know how to merge properly, we even had dozens of these little changes. This is completely ridiculous. We don't want to see any of that. All the matters is the final result. That's why we follow the "squash and merge" method when doing the final merge of a PR into the main branch. I.e., all the little commits of the PR get squashed into a single commit, and then that commit gets merged into main. But we don't want to see all these little intermediate steps. It just clutters everything. And note that if anyone is interested in seeing the details of all that, they can still see all of it by going to the github page for that PR.

Practically, when doing a squash and merge, before clicking on the "squash and merge" button, you must blank out the description and only keep the title. See #1185 (comment) and the links there.

Does that make sense?

I understand, but why does this actually matter? Does anyone ever look at the git log

[felixpernegger]

@felixpernegger @Moniker1998 @yhx-12243 One other thing. You added the theorem [ ordinal + hereditarily realcompact => countable ].

The title of the PR mentions another theorem [ ordinal + hereditarily paracompact => countable ], which is also true, but is not deducible from other results in pi-base.

Any reason why we don't want to add that one?

Just put in the wrong title accidentally

[prabau]

I understand, but why does this actually matter? Does anyone ever look at the git log

@felixpernegger
I (and others in the past) use git log regularly. It's very convenient on the command line to look for things:
git log | grep ....
In any case, it does not hurt to follow that. And again, all the (mostly useless) information is still available if anyone cares.
So it would be much appreciated if you follow that guideline.