pi-base
Add realcompactification of Rudin's space and basic properties
See #1139
While I'm not confident about Rudin's original proof that this space is ultraparacompact, I am confident that it is ultraparacompact. See those notes by K. P. Hart (maybe I should add those as a reference?).
It seems that you forgot to add ~T5.
Yes, although #1135 is still open, so I'm not sure if I want to add this in this PR
It seems that you forgot to add ~T5.
Yes, although #1135 is still open, so I'm not sure if I want to add this in this PR
#1135 is solved now, it seems you can added {S208|P8} now.
I thought "realcompactification" always refers to Hewitt realcompactification. Is there another one?
If not, the shorter name "Realcompactification of Rudin's Dowker space" would be better.
@prabau Just as "compactification" doesn't always refer to Stone-Cech compactification, similarly "realcompactification" doesn't always refer to Hewitt realcompactification.