Katetov's non-normal subspace of $\beta\mathbb{N}$

[Moniker1998]

#360

[prabau]

github is complaining "The head ref may contain hidden characters ...", due to Katetov's name in there. But at least pi-base accepts the name for the preview mode.

FYI for future PRs: (although it may work in this case)
In the past we have had cases for example where someone had put a vertical bar in the branch name, and it was impossible to do anything with git, because the vertical bar was interpreted in a special way. It's better to limit the name to ascii characters and some of the non-alphanumeric characters should be avoided.

[Moniker1998]

Someone added S214 so sadly I need to resolve conflicts now...

[felixpernegger]

P6 can be removed (is automatically deduced)

[Moniker1998]

@felixpernegger do you want to verify this PR too? It's the oldest one from the open PR's

[felixpernegger]

ok

[Moniker1998]

@felixpernegger I think it would be productive to finish existing PR's.

[felixpernegger]

I review this now

[felixpernegger]

This seems like quite a tricky subspace. PR is mostly good, but especially P4 needs some changes. Thanks!

[prabau]

For some reason, I am unable to see this branch in the preview mode of the browser.

Is it working for you?

[felixpernegger]

it works for me if i click on copy there and paste that in

[prabau]

thanks for the suggestion. I tried that, even after clearing the browser cache, but no luck.
I'll have to do it manually in the preview pane

[Moniker1998]

So instead of the old properties which I added, I've added submetrizable etc. and this shows this space is hereditarily realcompact on its own. (note this is not supposed to be an attempt at "completion" of this space so no need to add too many traits)

[felixpernegger]

Looks good now