Add realcompactification of Rudin's space and basic properties

spaces/S000138/README.md

@@ -8,6 +8,6 @@ refs:
     name: Dowker spaces (M.E. Rudin)
 ---
 
-Rudin's Dowker space $X$ is the subset of the product $\Pi_{n\in\omega}(\omega_{n+1}+1)$ with the box topology consisting of all functions $f$ such that, for some $i$, we have $\omega< cf(f(n))<\omega_i$ for all $n\in\omega$.  
+Rudin's Dowker space $X$ is the subset of the product $\prod_{n\in\omega}(\omega_{n+1}+1)$ with the box topology consisting of all functions $f$ such that, for some $i$, we have $\omega< \text{cf}(f(n))<\omega_i$ for all $n\in\omega$.  
 
 See {{doi:10.4064/fm-73-2-179-186}} and section 3.2(i) of {{mr:0776636}}.

spaces/S000208/README.md

@@ -0,0 +1,13 @@
+---
+uid: S000208
+name: Hewitt realcompactification of Rudin's Dowker space
+refs:
+  - doi: 10.4064/fm-73-2-179-186
+    name: A normal space X for which X×I is not normal (M.E. Rudin)
+  - doi: 10.1007/978-1-4615-7819-2
+    name: Rings of Continuous Functions (Gillman & Jerison)
+---
+
+Hewitt realcompactification of {S138} $X'$ is the subset of the product $\prod_{n\in\omega}(\omega_{n+1}+1)$ with the box topology consisting of all functions $f$ such that $\omega< \text{cf}(f(n))$ for all $n\in\omega$. If $X$ denotes {S138}, then $\nu X = X'$ where $\nu Y$ denotes the Hewitt realcompactification of Tychonoff space $Y$ (see chapter 8 of {{doi:10.1007/978-1-4615-7819-2}} for definition of Hewitt realcompactification).
+
+Defined in {{doi:10.4064/fm-73-2-179-186}}.

spaces/S000208/properties/P000003.md

@@ -0,0 +1,10 @@
+---
+space: S000208
+property: P000003
+value: true
+refs:
+  - zb: "0951.54001"
+    name: Topology (Munkres)
+---
+
+Is a subspace of $\prod_n (\omega_n+1)$ with box topology, which is Hausdorff (theorem 19.4 of {{zb:0951.54001}}).

spaces/S000208/properties/P000008.md

@@ -0,0 +1,7 @@
+---
+space: S000208
+property: P000008
+value: false
+---
+
+Contains {S138} and {S138|P8}.

spaces/S000208/properties/P000114.md

@@ -0,0 +1,7 @@
+---
+space: S000208
+property: P000114
+value: false
+---
+
+Has {S138} as a subspace, and {S138|P114} and {S138|P57}.

spaces/S000208/properties/P000146.md

@@ -0,0 +1,10 @@
+---
+space: S000208
+property: P000146
+value: true
+refs:
+- doi: 10.4064/fm-73-2-179-186
+  name: A normal space X for which X×I is not normal (M.E. Rudin)
+---
+
+See IV.4 of {{doi:10.4064/fm-73-2-179-186}}.

spaces/S000208/properties/P000147.md

@@ -0,0 +1,10 @@
+---
+space: S000208
+property: P000147
+value: true
+refs:
+- doi: 10.4064/fm-73-2-179-186
+  name: A normal space X for which X×I is not normal (M.E. Rudin)
+---
+
+The proof is the same as for {S138}. See lemma 4 in {{doi:10.4064/fm-73-2-179-186}}.

spaces/S000208/properties/P000164.md

@@ -0,0 +1,7 @@
+---
+space: S000208
+property: P000164
+value: true
+---
+
+$|X| \leq \aleph_\omega^\omega$ and $\aleph_\omega^\omega$ is smaller than every measurable cardinal.