From b10b4fcad19044ae9ed8562abcd74dd176eee725 Mon Sep 17 00:00:00 2001
From: yhx-12243 <yhx12243@gmail.com>
Date: Fri, 16 Jan 2026 08:01:55 +0800
Subject: [PATCH 1/4] =?UTF-8?q?Has=20closed=20discrete=20subset=20of=20siz?=
 =?UTF-8?q?e=20=F0=9D=94=A0=20(part=203)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 spaces/S000060/properties/P000032.md | 16 ----------------
 spaces/S000070/properties/P000032.md | 10 ----------
 spaces/S000074/properties/P000032.md | 10 ----------
 theorems/T000309.md                  | 18 ++++++++++++++++++
 4 files changed, 18 insertions(+), 36 deletions(-)
 delete mode 100644 spaces/S000060/properties/P000032.md
 delete mode 100644 spaces/S000070/properties/P000032.md
 delete mode 100644 spaces/S000074/properties/P000032.md
 create mode 100644 theorems/T000309.md

diff --git a/spaces/S000060/properties/P000032.md b/spaces/S000060/properties/P000032.md
deleted file mode 100644
index 5bd56ca4e..000000000
--- a/spaces/S000060/properties/P000032.md
+++ /dev/null
@@ -1,16 +0,0 @@
----
-space: S000060
-property: P000032
-value: false
----
-
-Take any countable partition $\{A_n:n<\omega\}$ of $\mathbb R\setminus\mathbb Q$ into Euclidean-dense subsets.
-Then $\mathscr U:=\{A_n\cup\mathbb Q: n<\omega\}$ is
-a countable open cover of $X$. Let $\mathscr V$ be an open refinement of $\mathscr U$.
-Let $U$ be any neighbourhood of $x\in\mathbb R\setminus\mathbb Q$. The closure of $U$ contains an
-interval around $x$, hence for each $n<\omega$ there exists
-$a_n\in A_n\cap \overline{U}$.
-If $a_n\in V\in\mathscr V$, the open set $V$ intersects $U$.
-Note that each $a_n$ is contained in a different element of $\mathscr V$.
-Therefore $U$ intersects infinitely many elements of $\mathscr V$,
-proving $\mathscr V$ is not locally finite.
diff --git a/spaces/S000070/properties/P000032.md b/spaces/S000070/properties/P000032.md
deleted file mode 100644
index 1a7131dd9..000000000
--- a/spaces/S000070/properties/P000032.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000070
-property: P000032
-value: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-See item #8 for space #78 in {{zb:0386.54001}}.
diff --git a/spaces/S000074/properties/P000032.md b/spaces/S000074/properties/P000032.md
deleted file mode 100644
index 380aabcb6..000000000
--- a/spaces/S000074/properties/P000032.md
+++ /dev/null
@@ -1,10 +0,0 @@
----
-space: S000074
-property: P000032
-value: false
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
----
-
-See item #7 for space #82 in {{zb:0386.54001}}.
diff --git a/theorems/T000309.md b/theorems/T000309.md
new file mode 100644
index 000000000..432bc9e3a
--- /dev/null
+++ b/theorems/T000309.md
@@ -0,0 +1,18 @@
+---
+uid: T000309
+if:
+  and:
+  - P000026: true
+  - P000227: true
+then:
+  P000032: false
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+  - zb: "1116.54006"
+    name: Normality and countable paracompactness of hyperspaces of ordinals. (Kemoto, Nobuyuki)
+---
+
+See Exercise 5.2.C(b) in {{zb:0684.54001}}.
+
+See also Claim in {{zb:1116.54006}}.

From 0d2bae645b2cf6e2c6a7c80bee7415b1e2858c7c Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Fri, 16 Jan 2026 14:51:50 -0500
Subject: [PATCH 2/4] T309 -> T838

---
 theorems/{T000309.md => T000838.md} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename theorems/{T000309.md => T000838.md} (96%)

diff --git a/theorems/T000309.md b/theorems/T000838.md
similarity index 96%
rename from theorems/T000309.md
rename to theorems/T000838.md
index 432bc9e3a..31492b7a6 100644
--- a/theorems/T000309.md
+++ b/theorems/T000838.md
@@ -1,5 +1,5 @@
 ---
-uid: T000309
+uid: T000838
 if:
   and:
   - P000026: true

From 0b077a2b8335e56e2080c2e9e7907e0fe4894d13 Mon Sep 17 00:00:00 2001
From: yhx-12243 <yhx12243@gmail.com>
Date: Tue, 20 Jan 2026 13:47:42 +0800
Subject: [PATCH 3/4] Update theorems/T000838.md

Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
---
 theorems/T000838.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000838.md b/theorems/T000838.md
index 31492b7a6..568d24a06 100644
--- a/theorems/T000838.md
+++ b/theorems/T000838.md
@@ -15,4 +15,4 @@ refs:
 
 See Exercise 5.2.C(b) in {{zb:0684.54001}}.
 
-See also Claim in {{zb:1116.54006}}.
+See also the Claim on page 359 of {{zb:1116.54006}}.

From 5cc4c9df8283a8fe3c7d069dfa3ec170b3125182 Mon Sep 17 00:00:00 2001
From: yhx-12243 <yhx12243@gmail.com>
Date: Tue, 20 Jan 2026 13:48:51 +0800
Subject: [PATCH 4/4] Update T000838.md

---
 theorems/T000838.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theorems/T000838.md b/theorems/T000838.md
index 568d24a06..b00e53cfe 100644
--- a/theorems/T000838.md
+++ b/theorems/T000838.md
@@ -10,7 +10,7 @@ refs:
   - zb: "0684.54001"
     name: General Topology (Engelking, 1989)
   - zb: "1116.54006"
-    name: Normality and countable paracompactness of hyperspaces of ordinals. (Kemoto, Nobuyuki)
+    name: Normality and countable paracompactness of hyperspaces of ordinals. (N. Kemoto)
 ---
 
 See Exercise 5.2.C(b) in {{zb:0684.54001}}.