pi-base · prabau · Feb 14, 2026 · Feb 7, 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.
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.
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.