From 4be839fdd75281c5ddd16690cb3ccf275ecd813b Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Wed, 26 Aug 2026 02:44:46 -0400
Subject: [PATCH 01/11] S215 Mysior plane

---
 spaces/S000215/README.md             | 19 +++++++++++++++++++
 spaces/S000215/properties/P000022.md |  7 +++++++
 spaces/S000215/properties/P000031.md |  7 +++++++
 spaces/S000215/properties/P000050.md |  7 +++++++
 spaces/S000215/properties/P000051.md |  8 ++++++++
 spaces/S000215/properties/P000061.md | 10 ++++++++++
 spaces/S000215/properties/P000062.md |  7 +++++++
 spaces/S000215/properties/P000063.md |  7 +++++++
 spaces/S000215/properties/P000065.md |  7 +++++++
 spaces/S000215/properties/P000093.md |  7 +++++++
 spaces/S000215/properties/P000105.md | 10 ++++++++++
 spaces/S000215/properties/P000110.md | 14 ++++++++++++++
 spaces/S000215/properties/P000120.md |  7 +++++++
 spaces/S000215/properties/P000130.md |  7 +++++++
 spaces/S000215/properties/P000162.md | 10 ++++++++++
 spaces/S000215/properties/P000198.md |  7 +++++++
 16 files changed, 141 insertions(+)
 create mode 100644 spaces/S000215/README.md
 create mode 100644 spaces/S000215/properties/P000022.md
 create mode 100644 spaces/S000215/properties/P000031.md
 create mode 100644 spaces/S000215/properties/P000050.md
 create mode 100644 spaces/S000215/properties/P000051.md
 create mode 100644 spaces/S000215/properties/P000061.md
 create mode 100644 spaces/S000215/properties/P000062.md
 create mode 100644 spaces/S000215/properties/P000063.md
 create mode 100644 spaces/S000215/properties/P000065.md
 create mode 100644 spaces/S000215/properties/P000093.md
 create mode 100644 spaces/S000215/properties/P000105.md
 create mode 100644 spaces/S000215/properties/P000110.md
 create mode 100644 spaces/S000215/properties/P000120.md
 create mode 100644 spaces/S000215/properties/P000130.md
 create mode 100644 spaces/S000215/properties/P000162.md
 create mode 100644 spaces/S000215/properties/P000198.md

diff --git a/spaces/S000215/README.md b/spaces/S000215/README.md
new file mode 100644
index 0000000000..73dc94d42c
--- /dev/null
+++ b/spaces/S000215/README.md
@@ -0,0 +1,19 @@
+---
+uid: S000215
+name: Mysior plane
+refs:
+  - zb: "0469.54011"
+    name: A union of realcompact spaces (Mysior)
+  - zb: "1265.54111"
+    name: r-realcompact spaces (Bhattacharya & Dey)
+---
+
+Let $X=\mathbb R^2$ with each point $(x,y)$ with $y\ne 0$ isolated
+and each point $(x,0)$ having as local base the collection of open sets $U_n(x)$ ($n=1,2,\dots$),
+where $U_n(x)$ is the union of the three line segments
+* $\{(x, y): -1/n < y < 1/n\}$,
+* $\{(x+1+y, y): 0 < y < 1/n\}$,
+* $\{(x+\sqrt{2}+y, -y) : 0 < y < 1/n\}$.
+
+Introduced by Mysior in {{zb:0469.54011}}.
+Also described in Example 5 of {{zb:1265.54111}}.
diff --git a/spaces/S000215/properties/P000022.md b/spaces/S000215/properties/P000022.md
new file mode 100644
index 0000000000..7537efe4c5
--- /dev/null
+++ b/spaces/S000215/properties/P000022.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000022
+value: false
+---
+
+$U_1(x)$ is clopen and homeomorphic to {S133} and {S133|P22}.
diff --git a/spaces/S000215/properties/P000031.md b/spaces/S000215/properties/P000031.md
new file mode 100644
index 0000000000..5de623b69d
--- /dev/null
+++ b/spaces/S000215/properties/P000031.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000031
+value: true
+---
+
+If $\mathcal{U}$ is an open cover of $X$, for each $x\in \mathbb{R}$ pick $n(x)$ such that $U_{n(x)}(x)\subseteq U$ for some $U\in\mathcal{U}$. Let $\mathcal{V} = \{U_{n(x)}(x) : x\in \mathbb{R}\}\cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_{n(x)}(x)\}$, then $\mathcal{V}$ is an open refinement of $\mathcal{U}$, and any point of $X$ is contained in at most two elements of $\mathcal{V}$.
diff --git a/spaces/S000215/properties/P000050.md b/spaces/S000215/properties/P000050.md
new file mode 100644
index 0000000000..e90b945d64
--- /dev/null
+++ b/spaces/S000215/properties/P000050.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000050
+value: true
+---
+
+Each $U_n(x)$ is clopen, as is each singleton $\{(x,y)\}$ with $y\ne 0$.
diff --git a/spaces/S000215/properties/P000051.md b/spaces/S000215/properties/P000051.md
new file mode 100644
index 0000000000..441002da02
--- /dev/null
+++ b/spaces/S000215/properties/P000051.md
@@ -0,0 +1,8 @@
+---
+space: S000215
+property: P000051
+value: true
+---
+
+If $Y\subseteq X$ is non-empty then either $Y$ contains a point $(x, y)$ with $y\neq 0$, so that $(x, y)$ is isolated in $Y$,
+or $Y\subseteq \mathbb{R}\times \{0\}$ and, since $U_n(x)\cap (\mathbb{R}\times \{0\}) = \{(x, 0)\}$, it follows that $Y$ is discrete.
diff --git a/spaces/S000215/properties/P000061.md b/spaces/S000215/properties/P000061.md
new file mode 100644
index 0000000000..531f3d8f3f
--- /dev/null
+++ b/spaces/S000215/properties/P000061.md
@@ -0,0 +1,10 @@
+---
+space: S000215
+property: P000061
+value: true
+---
+
+Note that if $V\subseteq X\setminus (\mathbb{R}\times \{0\})$ then $V = \bigcup_n V_n$ where $V_n = V\setminus(\mathbb{R}\times (-\frac{1}{n}, \frac{1}{n}))$ and each $V_n$ is clopen, so that $V$ is a cozero set as a countable union of cozero sets.
+
+If now $U\subseteq X$, let $V = X\setminus (U\cup (\mathbb{R}\times \{0\}))$.
+Then $V$ is a cozero set disjoint from $U$ and $U\cup V$ contains $X\setminus (\mathbb{R}\times \{0\})$ which is dense in $X$, so that $U\cup V$ is dense in $X$.
diff --git a/spaces/S000215/properties/P000062.md b/spaces/S000215/properties/P000062.md
new file mode 100644
index 0000000000..bc14a7fc45
--- /dev/null
+++ b/spaces/S000215/properties/P000062.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000062
+value: false
+---
+
+The open cover $\mathcal{U} = \{\mathbb{R}\times (-1, 1)\}\cup \{\{x\} : x\in X\setminus (\mathbb{R}\times (-1, 1))\}$ is a partition of $X$, and if there is a subfamily $\mathcal{V}\subseteq \mathcal{U}$ such that $\bigcup \mathcal{V}$ is dense, then $\mathcal{V} = \mathcal{U}$. Since $\mathcal{U}$ is uncountable, $X$ is not {P62}.
diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md
new file mode 100644
index 0000000000..7c485fbe6c
--- /dev/null
+++ b/spaces/S000215/properties/P000063.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000063
+value: true
+---
+
+Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$.
diff --git a/spaces/S000215/properties/P000065.md b/spaces/S000215/properties/P000065.md
new file mode 100644
index 0000000000..b894db47a6
--- /dev/null
+++ b/spaces/S000215/properties/P000065.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000065
+value: true
+---
+
+By definition.
diff --git a/spaces/S000215/properties/P000093.md b/spaces/S000215/properties/P000093.md
new file mode 100644
index 0000000000..3849a69356
--- /dev/null
+++ b/spaces/S000215/properties/P000093.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000093
+value: false
+---
+
+$U_n(x)$ is uncountable.
diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md
new file mode 100644
index 0000000000..18db3b7851
--- /dev/null
+++ b/spaces/S000215/properties/P000105.md
@@ -0,0 +1,10 @@
+---
+space: S000215
+property: P000105
+value: false
+refs:
+  - mathse: 412625
+    name: Answer to "Every bounded non countable subset of $\mathbb{R}$ has a two-sided accumulation point."
+---
+
+Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a point $x$ of $C$ such that for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction.
diff --git a/spaces/S000215/properties/P000110.md b/spaces/S000215/properties/P000110.md
new file mode 100644
index 0000000000..b09510bc0c
--- /dev/null
+++ b/spaces/S000215/properties/P000110.md
@@ -0,0 +1,14 @@
+---
+space: S000215
+property: P000110
+value: true
+refs:
+  - doi: 10.2991/978-94-6239-216-8
+    name: Generalized Metric Spaces and Mappings (S. Lin, Z. Yun)
+---
+
+By theorem 1.2.13 of {{doi:10.2991/978-94-6239-216-8}} it suffices to show that $X$ is quasi-developable and a {P132}. 
+
+If $A\subseteq X$, write $A = A_0\cup A_1$ where $A_0\subseteq \mathbb{R}\times \{0\}$ and $A_1\subseteq \mathbb{R}\times (\mathbb{R}\setminus \{0\})$. Then $A_1$ is open and $A_0 = \bigcap_n \bigcup_{x\in A_0} U_n(x)$ so that $A$ is a union of two $G_\delta$-sets, and so $G_\delta$ itself, showing that any subset of $X$ is a $G_\delta$-set. In particular $X$ is a {P132}.
+
+To show $X$ is quasi-developable, let $\mathcal{V} = \{\{x\} : x\in X\setminus (\mathbb{R}\times \{0\})\}$ and $\mathcal{A}_n^i = \{U_n(x) : x\in [3m+i, 3m+i+1), m\in\mathbb{N}\}$ where $i = 0, 1, 2$. Then $\{\mathcal{V}\}\cup \{\mathcal{A}_n^i : n\in\mathbb{N}, i = 0, 1, 2\}$ is a quasi-development for $X$.
diff --git a/spaces/S000215/properties/P000120.md b/spaces/S000215/properties/P000120.md
new file mode 100644
index 0000000000..73ed97c5c6
--- /dev/null
+++ b/spaces/S000215/properties/P000120.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000120
+value: true
+---
+
+$U_1(x)$ is homeomorphic to {S133} and {S133|P133}.
diff --git a/spaces/S000215/properties/P000130.md b/spaces/S000215/properties/P000130.md
new file mode 100644
index 0000000000..0b1f8e4e4a
--- /dev/null
+++ b/spaces/S000215/properties/P000130.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000130
+value: false
+---
+
+$U_n(x)$ is homeomorphic to {S133} and {S133|P130}
diff --git a/spaces/S000215/properties/P000162.md b/spaces/S000215/properties/P000162.md
new file mode 100644
index 0000000000..e592b0d950
--- /dev/null
+++ b/spaces/S000215/properties/P000162.md
@@ -0,0 +1,10 @@
+---
+space: S000215
+property: P000162
+value: false
+refs:
+  - mathse: 4718866
+    name: Mysior plane is not realcompact
+---
+
+Proved in {{mathse:4718866}}.
diff --git a/spaces/S000215/properties/P000198.md b/spaces/S000215/properties/P000198.md
new file mode 100644
index 0000000000..2d7e5b5688
--- /dev/null
+++ b/spaces/S000215/properties/P000198.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000198
+value: false
+---
+
+$\mathbb{R}\times \{0\}$ is an uncountable closed discrete subset of $X$

From 8ce92907bce0d53c21a179f99b8faebeef70caac Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Sun, 30 Aug 2026 07:05:35 +0200
Subject: [PATCH 02/11] Update spaces/S000215/properties/P000051.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000051.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spaces/S000215/properties/P000051.md b/spaces/S000215/properties/P000051.md
index 441002da02..c8a9ec4844 100644
--- a/spaces/S000215/properties/P000051.md
+++ b/spaces/S000215/properties/P000051.md
@@ -4,5 +4,5 @@ property: P000051
 value: true
 ---
 
-If $Y\subseteq X$ is non-empty then either $Y$ contains a point $(x, y)$ with $y\neq 0$, so that $(x, y)$ is isolated in $Y$,
-or $Y\subseteq \mathbb{R}\times \{0\}$ and, since $U_n(x)\cap (\mathbb{R}\times \{0\}) = \{(x, 0)\}$, it follows that $Y$ is discrete.
+Let $Y\subseteq X$ be non-empty. If $Y$ contains a point $(x, y)$ with $y\neq 0$, then $(x, y)$ is isolated in $Y$.
+Otherwise, $Y\subseteq \mathbb{R}\times \{0\}$ and, since $U_n(x)\cap (\mathbb{R}\times \{0\}) = \{(x, 0)\}$, it follows that $Y$ is discrete.

From 283c4cb965f8767b522da82491008d545a283ea0 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Sun, 30 Aug 2026 11:17:51 +0200
Subject: [PATCH 03/11] P22 hereditary clopen

---
 properties/P000022.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/properties/P000022.md b/properties/P000022.md
index 31209b8050..e83d013d70 100644
--- a/properties/P000022.md
+++ b/properties/P000022.md
@@ -15,3 +15,4 @@ Defined on page 20 of {{zb:0386.54001}}.
 
 - $X$ satisfies this property iff its Kolmogorov quotient $\mathrm{Kol}(X)$ does.
 - This property is preserved in any coarser topology.
+- This property is hereditary with respect to clopen sets.

From da68c0c7e86f12556d534e4e1532cbaed23082a6 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Mon, 31 Aug 2026 00:45:22 -0400
Subject: [PATCH 04/11] replace P130 with P23 trait

---
 spaces/S000215/properties/P000023.md | 8 ++++++++
 spaces/S000215/properties/P000130.md | 7 -------
 2 files changed, 8 insertions(+), 7 deletions(-)
 create mode 100644 spaces/S000215/properties/P000023.md
 delete mode 100644 spaces/S000215/properties/P000130.md

diff --git a/spaces/S000215/properties/P000023.md b/spaces/S000215/properties/P000023.md
new file mode 100644
index 0000000000..6839d186c3
--- /dev/null
+++ b/spaces/S000215/properties/P000023.md
@@ -0,0 +1,8 @@
+---
+space: S000215
+property: P000023
+value: false
+---
+
+The closed set $\{0\}\times[0,1)\subseteq X$ is homeomorphic to {S133}
+and {S133|P23}.
diff --git a/spaces/S000215/properties/P000130.md b/spaces/S000215/properties/P000130.md
deleted file mode 100644
index 0b1f8e4e4a..0000000000
--- a/spaces/S000215/properties/P000130.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000215
-property: P000130
-value: false
----
-
-$U_n(x)$ is homeomorphic to {S133} and {S133|P130}

From 14f86a7b7b4fb31c690e2dfa901e7b3251a9c26b Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Mon, 31 Aug 2026 08:56:26 +0200
Subject: [PATCH 05/11] swap extent to subset of size c

---
 spaces/S000215/properties/P000198.md | 7 -------
 spaces/S000215/properties/P000227.md | 7 +++++++
 2 files changed, 7 insertions(+), 7 deletions(-)
 delete mode 100644 spaces/S000215/properties/P000198.md
 create mode 100644 spaces/S000215/properties/P000227.md

diff --git a/spaces/S000215/properties/P000198.md b/spaces/S000215/properties/P000198.md
deleted file mode 100644
index 2d7e5b5688..0000000000
--- a/spaces/S000215/properties/P000198.md
+++ /dev/null
@@ -1,7 +0,0 @@
----
-space: S000215
-property: P000198
-value: false
----
-
-$\mathbb{R}\times \{0\}$ is an uncountable closed discrete subset of $X$
diff --git a/spaces/S000215/properties/P000227.md b/spaces/S000215/properties/P000227.md
new file mode 100644
index 0000000000..c845013fda
--- /dev/null
+++ b/spaces/S000215/properties/P000227.md
@@ -0,0 +1,7 @@
+---
+space: S000215
+property: P000227
+value: false
+---
+
+$\mathbb{R}\times \{0\}$ is an closed discrete subset of size $\mathfrak{c}$

From cdfd7270afdec0b90674413e77e610ba1260500f Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Tue, 1 Sep 2026 15:13:06 +0200
Subject: [PATCH 06/11] Update spaces/S000215/properties/P000227.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000227.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spaces/S000215/properties/P000227.md b/spaces/S000215/properties/P000227.md
index c845013fda..e9d6575cbf 100644
--- a/spaces/S000215/properties/P000227.md
+++ b/spaces/S000215/properties/P000227.md
@@ -1,7 +1,7 @@
 ---
 space: S000215
 property: P000227
-value: false
+value: true
 ---
 
-$\mathbb{R}\times \{0\}$ is an closed discrete subset of size $\mathfrak{c}$
+$\mathbb{R}\times \{0\}$ is a closed discrete subset of size $\mathfrak{c}$

From e03e0be3060bbef6297fbeca27594039631319cb Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Wed, 2 Sep 2026 13:43:12 +0200
Subject: [PATCH 07/11] changed para-Lindelof a little

---
 spaces/S000215/properties/P000105.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md
index 18db3b7851..4c0e9a82e5 100644
--- a/spaces/S000215/properties/P000105.md
+++ b/spaces/S000215/properties/P000105.md
@@ -7,4 +7,4 @@ refs:
     name: Answer to "Every bounded non countable subset of $\mathbb{R}$ has a two-sided accumulation point."
 ---
 
-Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a point $x$ of $C$ such that for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and $m$ such that $U_m(x)$ intersects countably many $U_n(y)$ for $y\in C$. Note that there is $z < x$ such that $U_n(y)\cap U_m(x)\neq \emptyset$ for all $y\in (z, x)\cap C$, and since $(z, x)\cap C$ is uncountable we obtain a contradiction.
+Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a two-sided accumulation point $x$ of $C$, that is for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and let $m$ be such that $U_m(x+1)$ intersects countably many $U_n(y)$ for $y\in C$. There is $y_0 < x$ such that $y_0 < y < x$ implies $U_n(y)\cap U_m(x+1)\neq\emptyset$ yet $C\cap (y_0, x)$ is uncountable, contradiction.

From 58e4dab3a5e39e22ef1330290d8cbd539d7df981 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Wed, 2 Sep 2026 13:51:32 +0200
Subject: [PATCH 08/11] Update spaces/S000215/properties/P000110.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000110.md | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/spaces/S000215/properties/P000110.md b/spaces/S000215/properties/P000110.md
index b09510bc0c..fb54499a0f 100644
--- a/spaces/S000215/properties/P000110.md
+++ b/spaces/S000215/properties/P000110.md
@@ -2,13 +2,9 @@
 space: S000215
 property: P000110
 value: true
-refs:
-  - doi: 10.2991/978-94-6239-216-8
-    name: Generalized Metric Spaces and Mappings (S. Lin, Z. Yun)
 ---
 
-By theorem 1.2.13 of {{doi:10.2991/978-94-6239-216-8}} it suffices to show that $X$ is quasi-developable and a {P132}. 
+A development for $X$ is given by the open covers $\mathscr U_1,\mathscr U_2,\dots$ with
 
-If $A\subseteq X$, write $A = A_0\cup A_1$ where $A_0\subseteq \mathbb{R}\times \{0\}$ and $A_1\subseteq \mathbb{R}\times (\mathbb{R}\setminus \{0\})$. Then $A_1$ is open and $A_0 = \bigcap_n \bigcup_{x\in A_0} U_n(x)$ so that $A$ is a union of two $G_\delta$-sets, and so $G_\delta$ itself, showing that any subset of $X$ is a $G_\delta$-set. In particular $X$ is a {P132}.
-
-To show $X$ is quasi-developable, let $\mathcal{V} = \{\{x\} : x\in X\setminus (\mathbb{R}\times \{0\})\}$ and $\mathcal{A}_n^i = \{U_n(x) : x\in [3m+i, 3m+i+1), m\in\mathbb{N}\}$ where $i = 0, 1, 2$. Then $\{\mathcal{V}\}\cup \{\mathcal{A}_n^i : n\in\mathbb{N}, i = 0, 1, 2\}$ is a quasi-development for $X$.
+$\quad\quad\mathscr U_n=\big\{U_n(x) : x\in\mathbb R\big\}
+\cup \big\{\{z\} : z\in X\setminus(\mathbb R\times\{0\}\big\}.$

From b5f414d475263758c3d6313986e6be20d11bf646 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Thu, 3 Sep 2026 10:25:01 +0200
Subject: [PATCH 09/11] Update spaces/S000215/properties/P000105.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000105.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/spaces/S000215/properties/P000105.md b/spaces/S000215/properties/P000105.md
index 4c0e9a82e5..ac38870a52 100644
--- a/spaces/S000215/properties/P000105.md
+++ b/spaces/S000215/properties/P000105.md
@@ -7,4 +7,7 @@ refs:
     name: Answer to "Every bounded non countable subset of $\mathbb{R}$ has a two-sided accumulation point."
 ---
 
-Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is para-Lindelof, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable. Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{y\in\mathbb{R} : n = n(x)\}$. Take a two-sided accumulation point $x$ of $C$, that is for any $y < x < z$ the sets $(y, x)\cap C$ and $(x, z)\cap C$ are uncountable (see {{mathse:412625}} for proof that such point exists), and let $m$ be such that $U_m(x+1)$ intersects countably many $U_n(y)$ for $y\in C$. There is $y_0 < x$ such that $y_0 < y < x$ implies $U_n(y)\cap U_m(x+1)\neq\emptyset$ yet $C\cap (y_0, x)$ is uncountable, contradiction.
+Let $\mathcal{U} = \{U_1(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_1(x)\}$. If $X$ is {P105}, then by taking a locally countable open refinement of $\mathcal{U}$, for every $x\in \mathbb{R}$ there is $n(x)\in\mathbb{N}$ such that $\{U_{n(x)}(x): x\in \mathbb{R}\}$ is locally countable.
+Find $n$ such that $n = n(x)$ for uncountably many $x\in\mathbb{R}$, and let $C = \{x\in\mathbb{R} : n = n(x)\}$.
+Take a left-sided condensation point $x'$ of $C$; that is, for any $x < x'$ the set $(x, x')\cap C$ is uncountable (see {{mathse:412625}} for a proof that such a point exists).
+Then each basic neighborhood $U_m(x'+1)$ of $x'+1$ intersects uncountably many $U_n(y)$ with $y\in C$ and close enough to the left of $x$, which contradicts the local countability condition above.

From 72f4e24349ae0bd47bdbcdd633dda1ae52cc97de Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Thu, 3 Sep 2026 22:37:28 +0200
Subject: [PATCH 10/11] Update spaces/S000215/properties/P000063.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000063.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md
index 7c485fbe6c..bc00f53255 100644
--- a/spaces/S000215/properties/P000063.md
+++ b/spaces/S000215/properties/P000063.md
@@ -4,4 +4,7 @@ property: P000063
 value: true
 ---
 
+$X$ is {P50} and {P51}, hence {P6}
+[(Explore)](https://topology.pi-base.org/spaces?q=Zero+dimensional%2BScattered%2B%7E%24T_%7B3+%5Cfrac%7B1%7D%7B2%7D%7D%24).
+
 Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$.

From f325d68a697b941ac232572130e6cbb156fac3b9 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Fri, 4 Sep 2026 20:37:49 +0200
Subject: [PATCH 11/11] Update spaces/S000215/properties/P000063.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 spaces/S000215/properties/P000063.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/spaces/S000215/properties/P000063.md b/spaces/S000215/properties/P000063.md
index bc00f53255..65379a56ea 100644
--- a/spaces/S000215/properties/P000063.md
+++ b/spaces/S000215/properties/P000063.md
@@ -7,4 +7,7 @@ value: true
 $X$ is {P50} and {P51}, hence {P6}
 [(Explore)](https://topology.pi-base.org/spaces?q=Zero+dimensional%2BScattered%2B%7E%24T_%7B3+%5Cfrac%7B1%7D%7B2%7D%7D%24).
 
-Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction. So $x_n\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq \sqrt{2}$. But as $[-\sqrt{2}+x_1, \sqrt{2}+x_1]$ is totally bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $x$. If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$.
+Let $\mathcal{U}_n = \{U_n(x) : x\in\mathbb{R}\} \cup \{\{y\} : y\in X\setminus \bigcup_{x\in \mathbb{R}} U_n(x)\}$. Suppose that $\mathcal{F}$ is a family of closed subsets of $X$ with finite intersection property, and such that for each $n$ there exists $F_n\in\mathcal{F}$ with $F_n\subseteq U$ for some $U\in\mathcal{U}_n$. If $U = \{y\}$, then $F_n = \{y\}$ and so $y\in \bigcap \mathcal{F}$. So we can assume that $F_n\subseteq U_n(x_n)$ where $x_n\in\mathbb{R}$. If $(x_n, 0)\notin F_n$, then $U_k(x_n)\cap F_n = \emptyset$ for some $k$, and so $F_n\subseteq X\setminus (\mathbb{R}\times (-\frac{1}{k}, \frac{1}{k}))$. And since $F_k\subseteq U_k(x_k)\subseteq \mathbb{R}\times (-\frac{1}{k}, \frac{1}{k})$, we must have $F_k\cap F_n = \emptyset$, which is a contradiction.
+So $(x_n,0)\in F_n$ for all $n$. Since $F_n\cap F_m\neq\emptyset$ it follows that $U_n(x_n)\cap U_m(x_m)\neq\emptyset$ and so $x_n = x_m$ or $1 < |x_n-x_m|\leq 1+\sqrt{2}$.
+But as the interval $[x_1-1-\sqrt{2}, x_1+1+\sqrt{2}]$ is bounded, the set $\{x_n : n\in\mathbb{N}\}$ must be finite, and so there is some $x\in\mathbb{R}$ such that $x_n = x$ for infinitely many $n$.
+If $F\in\mathcal{F}$, then $U_n(x)\cap F\supseteq F_n\cap F\neq\emptyset$ for infinitely many $n$, and so $U_n(x)\cap F\neq\emptyset$ for all $n$, which implies $(x, 0)\in F$ for all $F\in\mathcal{F}$ or in other words $(x, 0)\in\bigcap\mathcal{F}$.