From 3e0ac67340dab2db87004c6d4dae882500c442b3 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Tue, 9 Sep 2025 11:55:56 +0200
Subject: [PATCH 1/9] add three new theorems

---
 theorems/T000788.md |  9 +++++++++
 theorems/T000789.md | 15 +++++++++++++++
 theorems/T000790.md | 15 +++++++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 theorems/T000788.md
 create mode 100644 theorems/T000789.md
 create mode 100644 theorems/T000790.md

diff --git a/theorems/T000788.md b/theorems/T000788.md
new file mode 100644
index 0000000000..817e4b4989
--- /dev/null
+++ b/theorems/T000788.md
@@ -0,0 +1,9 @@
+---
+uid: T000788
+if:
+  P000110: true
+then:
+  P000117: true
+---
+
+Let $(\mathcal{U}_n)$ be development for $X$. Since every developable space is subparacompact, there exist a $\sigma$-locally finite closed refinement $\mathcal{V}_n$ of $\mathcal{U}_n$ for each $n$. Then $\mathcal{N} = \bigcup_n \mathcal{V}_n$ is $\sigma$-locally finite, and if $x\in W$ with $W$ open, then there is $n$ with $\text{St}(x, \mathcal{U}_n)\subseteq W$, and so $\text{St}(x, \mathcal{V}_n)\subseteq \text{St}(x, \mathcal{U}_n)\subseteq W$. Since $\mathcal{V}_n$ is a cover, it follows that there is $V\in\mathcal{V}_n$ with $x\in V\subseteq W$. So $\mathcal{N}$ is a $\sigma$-locally finite closed network.
diff --git a/theorems/T000789.md b/theorems/T000789.md
new file mode 100644
index 0000000000..61df8ee7c5
--- /dev/null
+++ b/theorems/T000789.md
@@ -0,0 +1,15 @@
+---
+uid: T000789
+if:
+  and:
+  - P000011: true
+  - P000028: true
+  - P000118: true
+then:
+  P000121: true
+refs:
+  - doi: 10.1002/mana.19700450103
+    name: A Metrization Theorem (P. O'Meara)
+---
+
+We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000790.md b/theorems/T000790.md
new file mode 100644
index 0000000000..229ee9977b
--- /dev/null
+++ b/theorems/T000790.md
@@ -0,0 +1,15 @@
+---
+uid: T000790
+if:
+  and:
+  - P000011: true
+  - P000130: true
+  - P000118: true
+then:
+  P000121: true
+refs:
+  - doi: 10.1002/mana.19700450103
+    name: A Metrization Theorem (P. O'Meara)
+---
+
+We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.

From 81de33fce1d0cbdea987c407766193336592f287 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Tue, 9 Sep 2025 12:38:24 +0200
Subject: [PATCH 2/9] replaced obsolete theorems

---
 theorems/T000516.md | 13 +++++++------
 theorems/T000517.md | 13 +++++++------
 theorems/T000789.md | 15 ---------------
 theorems/T000790.md | 15 ---------------
 4 files changed, 14 insertions(+), 42 deletions(-)
 delete mode 100644 theorems/T000789.md
 delete mode 100644 theorems/T000790.md

diff --git a/theorems/T000516.md b/theorems/T000516.md
index cd68d60dec..a442db20b7 100644
--- a/theorems/T000516.md
+++ b/theorems/T000516.md
@@ -2,13 +2,14 @@
 uid: T000516
 if:
   and:
-    - P000179: true
-    - P000028: true
+  - P000011: true
+  - P000028: true
+  - P000118: true
 then:
-  P000053: true
+  P000121: true
 refs:
-- zb: "0148.16701"
-  name: $\aleph_0$-spaces (E. Michael)
+  - doi: 10.1002/mana.19700450103
+    name: A Metrization Theorem (P. O'Meara)
 ---
 
-See result (B) in {{zb:0148.16701}} (<https://www.jstor.org/stable/24901448>).
+We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000517.md b/theorems/T000517.md
index aa9a67c328..26f10c1d4b 100644
--- a/theorems/T000517.md
+++ b/theorems/T000517.md
@@ -2,13 +2,14 @@
 uid: T000517
 if:
   and:
-    - P000179: true
-    - P000023: true
+  - P000011: true
+  - P000130: true
+  - P000118: true
 then:
-  P000053: true
+  P000121: true
 refs:
-- zb: "0148.16701"
-  name: $\aleph_0$-spaces (E. Michael)
+  - doi: 10.1002/mana.19700450103
+    name: A Metrization Theorem (P. O'Meara)
 ---
 
-See result (C) in {{zb:0148.16701}} (<https://www.jstor.org/stable/24901448>).
+We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000789.md b/theorems/T000789.md
deleted file mode 100644
index 61df8ee7c5..0000000000
--- a/theorems/T000789.md
+++ /dev/null
@@ -1,15 +0,0 @@
----
-uid: T000789
-if:
-  and:
-  - P000011: true
-  - P000028: true
-  - P000118: true
-then:
-  P000121: true
-refs:
-  - doi: 10.1002/mana.19700450103
-    name: A Metrization Theorem (P. O'Meara)
----
-
-We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000790.md b/theorems/T000790.md
deleted file mode 100644
index 229ee9977b..0000000000
--- a/theorems/T000790.md
+++ /dev/null
@@ -1,15 +0,0 @@
----
-uid: T000790
-if:
-  and:
-  - P000011: true
-  - P000130: true
-  - P000118: true
-then:
-  P000121: true
-refs:
-  - doi: 10.1002/mana.19700450103
-    name: A Metrization Theorem (P. O'Meara)
----
-
-We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.

From 6b5dce33802456dd503883861c320a19663cd446 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Fri, 12 Sep 2025 09:01:05 +0200
Subject: [PATCH 3/9] added Kolmogorov

---
 properties/P000028.md | 1 +
 properties/P000118.md | 5 +++++
 properties/P000178.md | 5 +++++
 3 files changed, 11 insertions(+)

diff --git a/properties/P000028.md b/properties/P000028.md
index 5bae15f1c6..1b517f5979 100644
--- a/properties/P000028.md
+++ b/properties/P000028.md
@@ -16,3 +16,4 @@ Defined on page 7 of {{doi:10.1007/978-1-4612-6290-9}}.
 - This property is hereditary.
 - A space that is locally {P28} (every point has a neighborhood with the property)
 has the property.
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/properties/P000118.md b/properties/P000118.md
index f41503d578..043685d5b9 100644
--- a/properties/P000118.md
+++ b/properties/P000118.md
@@ -11,3 +11,8 @@ A space with a $\sigma$-locally finite $k$-network.
 A family $\mathcal N$ of subsets of $X$ is called a *$k$-network* if for every compact set $K$ and open set $U$ in $X$ with $K\subseteq U$, there exists a finite $\mathcal{N}^* \subseteq \mathcal{N}$ with $K \subseteq \bigcup\mathcal{N}^* \subseteq U$.  The family $\mathcal N$ is *$\sigma$-locally finite* if it is a countable union of locally finite families.
 
 See for example Definition 2.1 in {{doi:10.1016/j.topol.2015.05.085}}.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/properties/P000178.md b/properties/P000178.md
index 3c223d81ab..0b00ec98e4 100644
--- a/properties/P000178.md
+++ b/properties/P000178.md
@@ -11,3 +11,8 @@ refs:
 A space that is {P5} and {P118}.
 
 The notion was introduced in {{doi:10.1090/S0002-9939-1971-0276919-3}}.
+
+----
+#### Meta-properties
+
+- The Kolmogorov quotient $\text{Kol}(X)$ is {P178} iff $X$ is {P11} and {P118}.

From 03d3aa9c3afbfeea46df54a8ed30e665322f6a4f Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Tue, 30 Dec 2025 21:55:07 +0100
Subject: [PATCH 4/9] changed theorems to allow redundancy

---
 theorems/T000516.md |  7 +++----
 theorems/T000517.md |  7 +++----
 theorems/T000820.md | 12 ++++++++++++
 theorems/T000821.md | 12 ++++++++++++
 4 files changed, 30 insertions(+), 8 deletions(-)
 create mode 100644 theorems/T000820.md
 create mode 100644 theorems/T000821.md

diff --git a/theorems/T000516.md b/theorems/T000516.md
index a442db20b7..591caad474 100644
--- a/theorems/T000516.md
+++ b/theorems/T000516.md
@@ -2,14 +2,13 @@
 uid: T000516
 if:
   and:
-  - P000011: true
+  - P000178: true
   - P000028: true
-  - P000118: true
 then:
-  P000121: true
+  P000053: true
 refs:
   - doi: 10.1002/mana.19700450103
     name: A Metrization Theorem (P. O'Meara)
 ---
 
-We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
+The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000517.md b/theorems/T000517.md
index 26f10c1d4b..37ee7bec6a 100644
--- a/theorems/T000517.md
+++ b/theorems/T000517.md
@@ -2,14 +2,13 @@
 uid: T000517
 if:
   and:
-  - P000011: true
+  - P000178: true
   - P000130: true
-  - P000118: true
 then:
-  P000121: true
+  P000053: true
 refs:
   - doi: 10.1002/mana.19700450103
     name: A Metrization Theorem (P. O'Meara)
 ---
 
-We can assume $X$ is a {P178} by taking Komogorov quotient. The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
+Follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
diff --git a/theorems/T000820.md b/theorems/T000820.md
new file mode 100644
index 0000000000..86f8c2cb43
--- /dev/null
+++ b/theorems/T000820.md
@@ -0,0 +1,12 @@
+---
+uid: T000820
+if:
+  and:
+  - P000011: true
+  - P000028: true
+  - P000118: true
+then:
+  P000121: true
+---
+
+Follows from {T516} by taking Komogorov quotient.
diff --git a/theorems/T000821.md b/theorems/T000821.md
new file mode 100644
index 0000000000..b4859cac69
--- /dev/null
+++ b/theorems/T000821.md
@@ -0,0 +1,12 @@
+---
+uid: T000821
+if:
+  and:
+  - P000011: true
+  - P000023: true
+  - P000118: true
+then:
+  P000121: true
+---
+
+Follows from {T517} by taking Komogorov quotient.

From 3a2bbb0512d578a32b18a21dec747d644802f227 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Wed, 31 Dec 2025 09:29:23 +0100
Subject: [PATCH 5/9] Update theorems/T000820.md

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

diff --git a/theorems/T000820.md b/theorems/T000820.md
index 86f8c2cb43..6c23ea1d33 100644
--- a/theorems/T000820.md
+++ b/theorems/T000820.md
@@ -9,4 +9,4 @@ then:
   P000121: true
 ---
 
-Follows from {T516} by taking Komogorov quotient.
+Follows from {T516} by taking Kolmogorov quotient.

From 5a2741144292da8082d7db9d15f5db90ba291a37 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Wed, 31 Dec 2025 11:53:57 +0100
Subject: [PATCH 6/9] rewrote T516 and T517

---
 theorems/T000516.md | 2 +-
 theorems/T000517.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theorems/T000516.md b/theorems/T000516.md
index 591caad474..2ca9ab56d8 100644
--- a/theorems/T000516.md
+++ b/theorems/T000516.md
@@ -11,4 +11,4 @@ refs:
     name: A Metrization Theorem (P. O'Meara)
 ---
 
-The theorem follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
+Established in theorem 1 of {{doi:10.1002/mana.19700450103}}, see remarks after definition 2.
diff --git a/theorems/T000517.md b/theorems/T000517.md
index 37ee7bec6a..ebe5f63375 100644
--- a/theorems/T000517.md
+++ b/theorems/T000517.md
@@ -11,4 +11,4 @@ refs:
     name: A Metrization Theorem (P. O'Meara)
 ---
 
-Follows from a more general result for $r$-spaces in {{doi:10.1002/mana.19700450103}}.
+Established in theorem 1 of {{doi:10.1002/mana.19700450103}}, see remarks after definition 2.

From 78b61257bd51c6a862a197c14a824ee0d3837ceb Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Thu, 1 Jan 2026 06:37:55 +0100
Subject: [PATCH 7/9] changed

---
 properties/P000132.md | 5 +++++
 theorems/T000821.md   | 8 ++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/properties/P000132.md b/properties/P000132.md
index 5290f3e9f5..9b3fc7ee59 100644
--- a/properties/P000132.md
+++ b/properties/P000132.md
@@ -18,3 +18,8 @@ Equivalently, a space in which every open set is an $F_\sigma$ set (a countable
 Defined on page 162 of {{doi:10.1007/978-1-4612-6290-9}}.
 
 Note: A $G_\delta$ space is sometimes called a "perfect space" (Exercise 1.5.H(a) in {{zb:0684.54001}}). Not to be be confused with a space that is a "perfect" in the sense of "perfect set" (= a set equal to its derived set = a closed set that is dense-in-itself), that is, a space without isolated point. See the discussion in <https://en.wikipedia.org/wiki/Talk:Perfect_set#Terminology_issue>.
+
+----
+#### Meta-properties
+
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
diff --git a/theorems/T000821.md b/theorems/T000821.md
index b4859cac69..f3fe13c0b1 100644
--- a/theorems/T000821.md
+++ b/theorems/T000821.md
@@ -2,11 +2,11 @@
 uid: T000821
 if:
   and:
-  - P000011: true
   - P000023: true
-  - P000118: true
+  - P000134: true
+  - P000132: true
 then:
-  P000121: true
+  P000028: true
 ---
 
-Follows from {T517} by taking Komogorov quotient.
+Follows from {T503} by taking Kolmogorov quotient.

From cb1639058e325fe748f461fb3921ee20a41bd0e6 Mon Sep 17 00:00:00 2001
From: Moniker1998 <adamcz98333@gmail.com>
Date: Thu, 1 Jan 2026 07:27:39 +0100
Subject: [PATCH 8/9] changed

---
 theorems/T000517.md | 12 +++++-------
 theorems/T000821.md | 12 ------------
 2 files changed, 5 insertions(+), 19 deletions(-)
 delete mode 100644 theorems/T000821.md

diff --git a/theorems/T000517.md b/theorems/T000517.md
index ebe5f63375..d825cec6ff 100644
--- a/theorems/T000517.md
+++ b/theorems/T000517.md
@@ -2,13 +2,11 @@
 uid: T000517
 if:
   and:
-  - P000178: true
-  - P000130: true
+  - P000023: true
+  - P000134: true
+  - P000132: true
 then:
-  P000053: true
-refs:
-  - doi: 10.1002/mana.19700450103
-    name: A Metrization Theorem (P. O'Meara)
+  P000028: true
 ---
 
-Established in theorem 1 of {{doi:10.1002/mana.19700450103}}, see remarks after definition 2.
+Follows from {T503} by taking Kolmogorov quotient.
diff --git a/theorems/T000821.md b/theorems/T000821.md
deleted file mode 100644
index f3fe13c0b1..0000000000
--- a/theorems/T000821.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-uid: T000821
-if:
-  and:
-  - P000023: true
-  - P000134: true
-  - P000132: true
-then:
-  P000028: true
----
-
-Follows from {T503} by taking Kolmogorov quotient.

From 54979287f1845e88fef5b912844b891807e87011 Mon Sep 17 00:00:00 2001
From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com>
Date: Thu, 1 Jan 2026 07:47:30 +0100
Subject: [PATCH 9/9] Update theorems/T000788.md

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

diff --git a/theorems/T000788.md b/theorems/T000788.md
index 817e4b4989..3f9b4bcefa 100644
--- a/theorems/T000788.md
+++ b/theorems/T000788.md
@@ -6,4 +6,4 @@ then:
   P000117: true
 ---
 
-Let $(\mathcal{U}_n)$ be development for $X$. Since every developable space is subparacompact, there exist a $\sigma$-locally finite closed refinement $\mathcal{V}_n$ of $\mathcal{U}_n$ for each $n$. Then $\mathcal{N} = \bigcup_n \mathcal{V}_n$ is $\sigma$-locally finite, and if $x\in W$ with $W$ open, then there is $n$ with $\text{St}(x, \mathcal{U}_n)\subseteq W$, and so $\text{St}(x, \mathcal{V}_n)\subseteq \text{St}(x, \mathcal{U}_n)\subseteq W$. Since $\mathcal{V}_n$ is a cover, it follows that there is $V\in\mathcal{V}_n$ with $x\in V\subseteq W$. So $\mathcal{N}$ is a $\sigma$-locally finite closed network.
+Let $(\mathcal{U}_n)$ be development for $X$. Since {T730}, there exist a $\sigma$-locally finite closed refinement $\mathcal{V}_n$ of $\mathcal{U}_n$ for each $n$. Then $\mathcal{N} = \bigcup_n \mathcal{V}_n$ is $\sigma$-locally finite, and if $x\in W$ with $W$ open, then there is $n$ with $\text{St}(x, \mathcal{U}_n)\subseteq W$, and so $\text{St}(x, \mathcal{V}_n)\subseteq \text{St}(x, \mathcal{U}_n)\subseteq W$. Since $\mathcal{V}_n$ is a cover, it follows that there is $V\in\mathcal{V}_n$ with $x\in V\subseteq W$. So $\mathcal{N}$ is a $\sigma$-locally finite network.