From 3138802f669c8c8ff82acb96c6976e6b4f2cce7f Mon Sep 17 00:00:00 2001 From: Batixx Date: Sat, 7 Feb 2026 16:59:03 +0100 Subject: [PATCH 1/6] traits --- spaces/S000017/properties/P000219.md | 7 +++++++ spaces/S000199/properties/P000219.md | 7 +++++++ spaces/S000200/properties/P000219.md | 7 +++++++ spaces/S000217/properties/P000219.md | 7 +++++++ 4 files changed, 28 insertions(+) create mode 100644 spaces/S000017/properties/P000219.md create mode 100644 spaces/S000199/properties/P000219.md create mode 100644 spaces/S000200/properties/P000219.md create mode 100644 spaces/S000217/properties/P000219.md diff --git a/spaces/S000017/properties/P000219.md b/spaces/S000017/properties/P000219.md new file mode 100644 index 0000000000..81fae0db79 --- /dev/null +++ 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 new file mode 100644 index 0000000000..bdd8acd31d --- /dev/null +++ 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 new file mode 100644 index 0000000000..0478a194d2 --- /dev/null +++ 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 new file mode 100644 index 0000000000..ab6e210575 --- /dev/null +++ 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. From 6421519f7ee8ffa22febc256792c5444b2fb498d Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Sun, 8 Feb 2026 04:29:14 +0100 Subject: [PATCH 2/6] Update spaces/S000017/properties/P000219.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- spaces/S000017/properties/P000219.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000017/properties/P000219.md b/spaces/S000017/properties/P000219.md index 81fae0db79..4d486a10b9 100644 --- a/spaces/S000017/properties/P000219.md +++ b/spaces/S000017/properties/P000219.md @@ -4,4 +4,4 @@ property: P000219 value: true --- -Let $Y\subseteq X$ with |Y|=|X|$. Then any bijection $f:Y\to X$ is a homeomorphism. +Let $Y\subseteq X$ with $|Y|=|X|$. Then any bijection $f:Y\to X$ is a homeomorphism. From 5ee3667ba058f9ee8cc826392e6d643b9c200b13 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Sun, 8 Feb 2026 15:37:46 +0100 Subject: [PATCH 3/6] typo --- spaces/S000199/properties/P000219.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000199/properties/P000219.md b/spaces/S000199/properties/P000219.md index bdd8acd31d..7842a0da2c 100644 --- a/spaces/S000199/properties/P000219.md +++ b/spaces/S000199/properties/P000219.md @@ -4,4 +4,4 @@ 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. From 0c2f03e9aa5d9953c195ce50d4aab129da6f3015 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Sun, 8 Feb 2026 15:38:03 +0100 Subject: [PATCH 4/6] typo --- spaces/S000200/properties/P000219.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000200/properties/P000219.md b/spaces/S000200/properties/P000219.md index 0478a194d2..713d1a1847 100644 --- a/spaces/S000200/properties/P000219.md +++ b/spaces/S000200/properties/P000219.md @@ -4,4 +4,4 @@ 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. From 974fcac7e0029b24915e770e4c612322187edf3a Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Sun, 8 Feb 2026 15:38:19 +0100 Subject: [PATCH 5/6] typo --- spaces/S000217/properties/P000219.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000217/properties/P000219.md b/spaces/S000217/properties/P000219.md index ab6e210575..a10995f6ec 100644 --- a/spaces/S000217/properties/P000219.md +++ b/spaces/S000217/properties/P000219.md @@ -4,4 +4,4 @@ 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. From 23921b9996ec3500431ab343330dd88bdcef1067 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 13 Feb 2026 13:52:54 +0100 Subject: [PATCH 6/6] apply suggestions Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- spaces/S000199/properties/P000219.md | 8 +++++++- spaces/S000200/properties/P000219.md | 8 +++++++- spaces/S000217/properties/P000219.md | 9 ++++++++- 3 files changed, 22 insertions(+), 3 deletions(-) diff --git a/spaces/S000199/properties/P000219.md b/spaces/S000199/properties/P000219.md index 7842a0da2c..49cefa08f8 100644 --- a/spaces/S000199/properties/P000219.md +++ b/spaces/S000199/properties/P000219.md @@ -4,4 +4,10 @@ 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|$. +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 index 713d1a1847..c775068d6f 100644 --- a/spaces/S000200/properties/P000219.md +++ b/spaces/S000200/properties/P000219.md @@ -4,4 +4,10 @@ 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|$. +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 index a10995f6ec..8d1c178100 100644 --- a/spaces/S000217/properties/P000219.md +++ b/spaces/S000217/properties/P000219.md @@ -4,4 +4,11 @@ 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|$. +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.