CWH locally relatively compact Alexandrov T0 spaces are normal

[prabau]

New T927: Collectionwise Hausdorff + locally relatively compact + Alexandrov + T0 => normal.

One of the contrapositives allows to derive that three more spaces are not CWH:
https://topology.pi-base.org/spaces?q=24%2Balexandrov%2BT0%2B%7Enormal%2B%3FCWH

(I initially added some meta-properties, thinking there would be a version without T0, but that did not work. I left them as it's good to have anyway.)

[felixpernegger]

Isnt T0 redundant

[felixpernegger]

It would really be good if #1725 was reviewed some day

[prabau]

Isnt T0 redundant

T0 is needed here. For example, take $Y$ = a space that is locally relatively compact, Alexandrov and not normal. Take the product $X=Y\times S$ with $S$ some indiscrete space with two points for example. The result is still locally relatively compact, Alexandrov and not normal, and is also collectionwise Hausdorff (because there are no closed points). But it is not T0.

[prabau]

It would really be good if #1725 was reviewed some day

That PR is just too tedious to review. But if you write a small PR at a time, each for say 10 properties, I'll be more than happy to review it. You can even wait until one gets merged before doing the next one. As always, small changes for incremental progress instead of "big bang" approach. It would be great if you could do that. Please!!!

[prabau]

@JSMassmann FYI

[felixpernegger]

It would really be good if #1725 was reviewed some day

That PR is just too tedious to review. But if you write a small PR at a time, each for say 10 properties, I'll be more than happy to review it. You can even wait until one gets merged before doing the next one. As always, small changes for incremental progress instead of "big bang" approach. It would be great if you could do that. Please!!!

I also have lots of open PRs that are very easy yet have gotten no reviews since they had been opened back in March or so

[JSMassmann]

LGTM