CWH locally relatively compact Alexandrov T0 spaces are normal

properties/P000024.md

@@ -15,4 +15,13 @@ Each point has a local base of neighborhoods with compact closure.
 Equivalently (see Condition 2 of {{wikipedia:Locally_compact_space}}), every point in $X$ has
 a closed and compact neighborhood.
 
-Defined on page 20 of {{zb:0386.54001}} as "strongly locally compact". Contrast with {P130}.
+Defined on page 20 of {{zb:0386.54001}} as "strongly locally compact".
+
+Compare with {P130}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
+- This property is hereditary with respect to closed sets.
+- This property is preserved by finite products.

properties/P000090.md

@@ -28,6 +28,7 @@ See also {{zb:0944.54018}}.
 ----
 #### Meta-properties
 
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
 - This property is hereditary.
 - This property is preserved by arbitrary disjoint unions.
 - This property is preserved by finite products.

theorems/T000927.md

@@ -0,0 +1,31 @@
+---
+uid: T000927
+if:
+  and:
+  - P000246: true
+  - P000024: true
+  - P000090: true
+  - P000001: true
+then:
+  P000013: true
+---
+
+We assume $X$ is {P24}, {P90}, {P1}
+and not {P13} and show it is not {P246}.
+
+*Notation*:  Write $x\le y$ when $x\in\overline{\{y\}}$ (specialization order).
+The smallest open neighborhoods of a point $a\in X$ and of a set $A\subseteq X$ are the upper sets
+${\uparrow}a:=\{x\in X:a\le x\}$ and ${\uparrow}A:=\bigcup_{a\in A}{\uparrow}a$.
+And let ${\downarrow}a:=\{x\in X:x\le a\}$.
+
+Let $A$ and $B$ be disjoint closed sets that don't have disjoint open neighborhoods.
+So ${\uparrow}A\cap{\uparrow}B\ne\emptyset$ and ${\uparrow}a\cap{\uparrow}b\ne\emptyset$
+for some $a\in A$ and $b\in B$.
+The set ${\downarrow}a$ is closed in $X$, hence {P24}.
+Since {T641}, there is a point $a_1\le a$ with $\{a_1\}$ closed in ${\downarrow}a$, hence closed in $X$.
+Similarly there is a point $b_1\le b$ with $\{b_1\}$ closed in $X$.
+The points $a_1$ and $b_1$ are distinct, because $a_1\in A$ and $b_1\in B$.
+The set $\{a_1,b_1\}$ is discrete and closed in $X$ and
+its points cannot be separated by disjoint open sets as
+${\uparrow}a_1\cap{\uparrow}b_1 \supseteq {\uparrow}a\cap{\uparrow}b\ne\emptyset$.
+This shows that $X$ is not {P246}.