Add proof for T28

[felixpernegger]

Closes #1708. The proof here is copied from @Moniker1998 and slightly adapted.

[prabau]

Slightly sloppy in the language used. Also, need more detail about one thing. How do we know there is a finite subcover $\mathcal{V}$? It's because A is also countably compact because it is a closed in X. So need to state something extra here.

[prabau]

The non-T0 version would also be true it seems:
[ R1 + countably compact + first countable => regular ]
and is currently not known in pi-base (and would imply the existing T28).

I am not pushing for it though. If one day we get pi-base to use Kolmogorov quotients automatically, this new version would be implicitly derivable from the existing T28 and the existing T28 would be sufficient and preferable (simpler).

[prabau]

marking this as requesting changes so it does not get accidentally merged

[prabau]

@felixpernegger Have you looked in mathse to see if there was a proof available? (I haven't)

[felixpernegger]

@felixpernegger Have you looked in mathse to see if there was a proof available? (I haven't)

no, but since this is a 1 paragraph proof a outside reference is more distracting than helpful in my opinion

[prabau]

https://math.stackexchange.com/questions/2379365/prove-that-a-countably-compact-first-countable-t-2-space-is-regular, but it's not complete so not exactly usable.

[felixpernegger]

The non-T0 version would also be true it seems: [ R1 + countably compact + first countable => regular ] and is currently not known in pi-base (and would imply the existing T28).

I am not pushing for it though. If one day we get pi-base to use Kolmogorov quotients automatically, this new version would be implicitly derivable from the existing T28 and the existing T28 would be sufficient and preferable (simpler).

I suppose we get no new traits out of the non-t0 generalisation? in this case i agree to focus on the t0 case

[prabau]

@felixpernegger are you planning to fix further things here or you are done?

[prabau]

Maybe no need to be so explicit about closed hereditariness, but we should implicitly indicate we are using it.
I want to suggest a few other things at the same time, style wise. Let me try to write this up separately first.

[prabau]

Should we add a sentence at the end: This shows that $X$ is {P11}.
(P11= regular, which is what this is showing) or is it good enough?

changes have been added, so the rest is minor.

[felixpernegger]

Should we add a sentence at the end: This shows that $X$ is {P11}. (P11= regular, which is what this is showing) or is it good enough?

Good enough...

[prabau]

@Moniker1998 should review

[Moniker1998]

@prabau perfect to me