T497: locally compact KC spaces are regular

[prabau]

New T497: Locally compact + KC ==> regular.

The contrapositive allows to deduce that three more spaces are not locally compact.

[StevenClontz]

Neat. In fact these spaces are completely regular, since weakly locally compact + regular (or just R1) => completely regular. But this is a slick proof and is probably the right way to assert this rather than a direct proof for completely regular.

And there are several examples we know of already that are not normal: https://topology.pi-base.org/spaces?q=kc+%2B+Locally+Compact+%2B+%7Enormal

We should add a note to https://topology.pi-base.org/properties/P000011 that "local neighborhood base of closed sets" is an equivalent characterization, and then I think this is ready to go.

[StevenClontz]

Couple relevant mathse things we could add as citations:

https://math.stackexchange.com/questions/4940156/must-locally-compact-and-weakly-hausdorff-spaces-be-regular

https://math.stackexchange.com/questions/3442837/show-that-every-locally-compact-hausdorff-space-is-regular/4940160

[prabau]

And as mentioned in the comment by David Gao to one of your mathse posts, the theorem is equivalent to [locally compact + KC ==> T2], which is also equivalent to [locally compact + KC ==> Tychonoff].

All that is deducible given the current version of T497. As the current proof of T497 is immediate, I think it's ok to use that. But in our next zoom meeting, we could possibly discuss this in general. i.e. Suppose a theorem concludes property A from a set of hypotheses, and then in combination with other theorems one can further deduce a stronger property B. When is it preferable to have the first theorem deduce B directly, and when is it not.