pi-base · felixpernegger · Feb 7, 2026 · Feb 8, 2026 · Feb 8, 2026 · Feb 8, 2026
diff --git a/spaces/S000017/properties/P000219.md b/spaces/S000017/properties/P000219.md
@@ -0,0 +1,7 @@
+---
+space: S000017
+property: P000219
+value: true
+---
+
+Let $Y\subseteq X$ with $|Y|=|X|$. Then any bijection $f:Y\to X$ is a homeomorphism.
diff --git a/spaces/S000199/properties/P000219.md b/spaces/S000199/properties/P000219.md
@@ -0,0 +1,7 @@
+---
+space: S000199
+property: P000219
+value: true
+---
+
+Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+There is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$(\leftarrow,y]_X\cap Y = (\leftarrow,y]_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+There is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$(\leftarrow,y]_X\cap Y = (\leftarrow,y]_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.
diff --git a/spaces/S000200/properties/P000219.md b/spaces/S000200/properties/P000219.md
@@ -0,0 +1,7 @@
+---
+space: S000200
+property: P000219
+value: true
+---
+
+Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+There is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$[y,\to)_X\cap Y = [y,\to)_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+There is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$[y,\to)_X\cap Y = [y,\to)_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.
diff --git a/spaces/S000217/properties/P000219.md b/spaces/S000217/properties/P000219.md
@@ -0,0 +1,7 @@
+---
+space: S000217
+property: P000219
+value: true
+---
+
+Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+Using well-orderedness and the fact that $\omega_1$ is an initial ordinal,
+one can show that there is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$(\leftarrow,y]_X\cap Y = (\leftarrow,y]_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.
-Let $Y\subseteq X$ with $|Y|=|X|$. By ordinal recursion, we can construct a (unique) order preserving bijection $f:Y \to X$ which then must be a homeomorphism.
+Let $Y\subseteq X$ with $|Y|=|X|$.
+Using well-orderedness and the fact that $\omega_1$ is an initial ordinal,
+one can show that there is a unique order isomorphism $f:Y\to X$.
+Since $X$ is Alexandrov, so is $Y$ with its subspace topology $\tau_Y$.
+The smallest $\tau_Y$-neighborhood of a point $y\in Y$ is
+$$(\leftarrow,y]_X\cap Y = (\leftarrow,y]_Y,$$
+which coincides with the smallest neighborhood of $y$ in the left ray topology of $Y$.
+This shows that $f$ is a homeomorphism.