From 69cf76e75c1a879293bd0503ec3163f222549bb9 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 17 Jun 2026 12:44:08 +0200
Subject: [PATCH 01/20] Finite topology property + simple theorems

---
 properties/P000245.md | 16 ++++++++++++++++
 theorems/T000908.md   |  9 +++++++++
 theorems/T000909.md   |  9 +++++++++
 theorems/T000910.md   |  9 +++++++++
 4 files changed, 43 insertions(+)
 create mode 100644 properties/P000245.md
 create mode 100644 theorems/T000908.md
 create mode 100644 theorems/T000909.md
 create mode 100644 theorems/T000910.md

diff --git a/properties/P000245.md b/properties/P000245.md
new file mode 100644
index 000000000..364410bce
--- /dev/null
+++ b/properties/P000245.md
@@ -0,0 +1,16 @@
+---
+uid: P000245
+name: Finite topology
+aliases:
+    - Has finitely many open sets
+---
+
+The cardinality of the topology on $(X, \tau)$ is finite, i.e. $|\tau| < \infty$. 
+
+Equivalently, the space has only finitely many open sets.
+
+----
+#### Meta-properties
+
+- This property is hereditary.
+- This property is preserved in any coarser topology.
\ No newline at end of file
diff --git a/theorems/T000908.md b/theorems/T000908.md
new file mode 100644
index 000000000..a9a6dfa68
--- /dev/null
+++ b/theorems/T000908.md
@@ -0,0 +1,9 @@
+---
+uid: T000908
+if:
+  P000078: true
+then:
+  P000245: true
+---
+
+By definition.
\ No newline at end of file
diff --git a/theorems/T000909.md b/theorems/T000909.md
new file mode 100644
index 000000000..003ac9446
--- /dev/null
+++ b/theorems/T000909.md
@@ -0,0 +1,9 @@
+---
+uid: T000909
+if:
+  P000245: true
+then:
+  P000226: true
+---
+
+Since there are finitely many open sets, there is no strictly decreasing infinite sequence of open sets, hence Artinian.
\ No newline at end of file
diff --git a/theorems/T000910.md b/theorems/T000910.md
new file mode 100644
index 000000000..f084dde38
--- /dev/null
+++ b/theorems/T000910.md
@@ -0,0 +1,9 @@
+---
+uid: T000910
+if:
+  P000245: true
+then:
+  P000208: true
+---
+
+Since there are finitely many open sets, there is no strictly increasing infinite sequence of open sets, hence Noetherian.
\ No newline at end of file

From fbc76b89bb2cf44ee6206aed87af38da910e6f79 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 17 Jun 2026 13:29:42 +0200
Subject: [PATCH 02/20] more simple theorems

---
 theorems/T000911.md |  9 +++++++++
 theorems/T000912.md | 12 ++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 theorems/T000911.md
 create mode 100644 theorems/T000912.md

diff --git a/theorems/T000911.md b/theorems/T000911.md
new file mode 100644
index 000000000..636aa655e
--- /dev/null
+++ b/theorems/T000911.md
@@ -0,0 +1,9 @@
+---
+uid: T000911
+if:
+  P000129: true
+then:
+  P000245: true
+---
+
+By definition.
\ No newline at end of file
diff --git a/theorems/T000912.md b/theorems/T000912.md
new file mode 100644
index 000000000..3770fcc89
--- /dev/null
+++ b/theorems/T000912.md
@@ -0,0 +1,12 @@
+---
+uid: T000912
+if:
+  and:
+    - P000245: true
+    - P000001: true
+then:
+  P000078: true
+---
+
+For any $x \in X$, define $U_x = \bigcap \{ U \in \tau : x \in U \}$ to be the minimal neighborhood of $x$. Since the topology is finite, the intersection is finite, so $U_x$ is open and hence in $\tau$. 
+The map $x \mapsto U_x$ is injective by $T_0$, so $|X| \leq |\{U_x : x \in X\}| \leq |\tau| < \infty$, so $X$ is finite.
\ No newline at end of file

From 14ba0362ecfbc622a4ecca24f63cddea913389be Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 17 Jun 2026 14:02:11 +0200
Subject: [PATCH 03/20] address comments, add newlines

---
 properties/P000245.md | 6 ++++--
 theorems/T000908.md   | 2 +-
 theorems/T000909.md   | 2 +-
 theorems/T000910.md   | 2 +-
 theorems/T000911.md   | 2 +-
 theorems/T000912.md   | 2 +-
 6 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/properties/P000245.md b/properties/P000245.md
index 364410bce..dd9490dcd 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -7,10 +7,12 @@ aliases:
 
 The cardinality of the topology on $(X, \tau)$ is finite, i.e. $|\tau| < \infty$. 
 
-Equivalently, the space has only finitely many open sets.
+Equivalently, the Kolmogorov quotient of the space is finite.
 
 ----
 #### Meta-properties
 
 - This property is hereditary.
-- This property is preserved in any coarser topology.
\ No newline at end of file
+- This property is preserved in any coarser topology.
+- The Kolmogorov quotient $\text{Kol}(X)$ is {P78} iff $X$ is {P245}.
+- This property is preserved by finite products.
diff --git a/theorems/T000908.md b/theorems/T000908.md
index a9a6dfa68..ed8e8caea 100644
--- a/theorems/T000908.md
+++ b/theorems/T000908.md
@@ -6,4 +6,4 @@ then:
   P000245: true
 ---
 
-By definition.
\ No newline at end of file
+By definition.
diff --git a/theorems/T000909.md b/theorems/T000909.md
index 003ac9446..78e0dd0bb 100644
--- a/theorems/T000909.md
+++ b/theorems/T000909.md
@@ -6,4 +6,4 @@ then:
   P000226: true
 ---
 
-Since there are finitely many open sets, there is no strictly decreasing infinite sequence of open sets, hence Artinian.
\ No newline at end of file
+Immediate from the definitions.
diff --git a/theorems/T000910.md b/theorems/T000910.md
index f084dde38..2dfb9cd9f 100644
--- a/theorems/T000910.md
+++ b/theorems/T000910.md
@@ -6,4 +6,4 @@ then:
   P000208: true
 ---
 
-Since there are finitely many open sets, there is no strictly increasing infinite sequence of open sets, hence Noetherian.
\ No newline at end of file
+Immediate from the definitions.
diff --git a/theorems/T000911.md b/theorems/T000911.md
index 636aa655e..61d0dcb10 100644
--- a/theorems/T000911.md
+++ b/theorems/T000911.md
@@ -6,4 +6,4 @@ then:
   P000245: true
 ---
 
-By definition.
\ No newline at end of file
+By definition.
diff --git a/theorems/T000912.md b/theorems/T000912.md
index 3770fcc89..5ff13e4fb 100644
--- a/theorems/T000912.md
+++ b/theorems/T000912.md
@@ -9,4 +9,4 @@ then:
 ---
 
 For any $x \in X$, define $U_x = \bigcap \{ U \in \tau : x \in U \}$ to be the minimal neighborhood of $x$. Since the topology is finite, the intersection is finite, so $U_x$ is open and hence in $\tau$. 
-The map $x \mapsto U_x$ is injective by $T_0$, so $|X| \leq |\{U_x : x \in X\}| \leq |\tau| < \infty$, so $X$ is finite.
\ No newline at end of file
+The map $x \mapsto U_x$ is injective by $T_0$, so $|X| \leq |\{U_x : x \in X\}| \leq |\tau| < \infty$, so $X$ is finite.

From 5e0cbc213279fe50f3321d4c15d8cc5998611948 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Wed, 17 Jun 2026 15:01:28 +0200
Subject: [PATCH 04/20] use kolmogorov

---
 theorems/T000912.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theorems/T000912.md b/theorems/T000912.md
index 5ff13e4fb..a7218743e 100644
--- a/theorems/T000912.md
+++ b/theorems/T000912.md
@@ -8,5 +8,4 @@ then:
   P000078: true
 ---
 
-For any $x \in X$, define $U_x = \bigcap \{ U \in \tau : x \in U \}$ to be the minimal neighborhood of $x$. Since the topology is finite, the intersection is finite, so $U_x$ is open and hence in $\tau$. 
-The map $x \mapsto U_x$ is injective by $T_0$, so $|X| \leq |\{U_x : x \in X\}| \leq |\tau| < \infty$, so $X$ is finite.
+Follows from Kolmogorov quotient being finite.

From d57741134fb8ea7a75c7fb5f8bd03e335017fabc Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Wed, 17 Jun 2026 16:16:34 -0400
Subject: [PATCH 05/20] Update properties/P000245.md

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

diff --git a/properties/P000245.md b/properties/P000245.md
index dd9490dcd..a83f52056 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -1,6 +1,6 @@
 ---
 uid: P000245
-name: Finite topology
+name: Has a finite topology
 aliases:
     - Has finitely many open sets
 ---

From 07ee004df8d53bd9ccc0654e98b41a94ac25f683 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Thu, 18 Jun 2026 09:03:24 +0200
Subject: [PATCH 06/20] Update theorems/T000908.md

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

diff --git a/theorems/T000908.md b/theorems/T000908.md
index ed8e8caea..485ca4078 100644
--- a/theorems/T000908.md
+++ b/theorems/T000908.md
@@ -6,4 +6,4 @@ then:
   P000245: true
 ---
 
-By definition.
+Immediate from the definition.

From e6f415cf32f57116f75d16c91ddfcfc6099b2a89 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Fri, 19 Jun 2026 19:35:24 +0200
Subject: [PATCH 07/20] Update properties/P000245.md

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

diff --git a/properties/P000245.md b/properties/P000245.md
index a83f52056..50eb98cb0 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -5,7 +5,7 @@ aliases:
     - Has finitely many open sets
 ---
 
-The cardinality of the topology on $(X, \tau)$ is finite, i.e. $|\tau| < \infty$. 
+$X$ has finitely many open sets.
 
 Equivalently, the Kolmogorov quotient of the space is finite.
 

From ecbda9c61e439c67dd6da3da3b534c14350beda2 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Fri, 19 Jun 2026 19:37:14 +0200
Subject: [PATCH 08/20] Update properties/P000245.md

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

diff --git a/properties/P000245.md b/properties/P000245.md
index 50eb98cb0..7adfcd3b1 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -14,5 +14,5 @@ Equivalently, the Kolmogorov quotient of the space is finite.
 
 - This property is hereditary.
 - This property is preserved in any coarser topology.
-- The Kolmogorov quotient $\text{Kol}(X)$ is {P78} iff $X$ is {P245}.
+- $X$ is {P245} iff its Kolmogorov quotient $\text{Kol}(X)$ is {P78}.
 - This property is preserved by finite products.

From 187f346fbb5b8fa5f31bf220665a46ccccc996c2 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Fri, 19 Jun 2026 19:38:13 +0200
Subject: [PATCH 09/20] Update properties/P000245.md

Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
---
 properties/P000245.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/properties/P000245.md b/properties/P000245.md
index 7adfcd3b1..9a61b1800 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -1,8 +1,8 @@
 ---
 uid: P000245
-name: Has a finite topology
+name: Has finitely many open sets
 aliases:
-    - Has finitely many open sets
+    - Has a finite topology
 ---
 
 $X$ has finitely many open sets.

From 3af82491ef6f993cc43fc2602ca0af829562e4ba Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Fri, 19 Jun 2026 19:45:52 +0200
Subject: [PATCH 10/20] Apply suggestion from @felixpernegger

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

diff --git a/theorems/T000912.md b/theorems/T000912.md
index a7218743e..d820c3d03 100644
--- a/theorems/T000912.md
+++ b/theorems/T000912.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Follows from Kolmogorov quotient being finite.
+Follows from the Kolmogorov quotient being finite.

From 0a5271d9a015d9d20b929b062bd77df54de78988 Mon Sep 17 00:00:00 2001
From: Felix Pernegger <s59fpern@uni-bonn.de>
Date: Fri, 19 Jun 2026 19:47:44 +0200
Subject: [PATCH 11/20] Apply suggestion from @felixpernegger

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

diff --git a/properties/P000245.md b/properties/P000245.md
index 9a61b1800..2e71d4d59 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -2,7 +2,7 @@
 uid: P000245
 name: Has finitely many open sets
 aliases:
-    - Has a finite topology
+  - Has a finite topology
 ---
 
 $X$ has finitely many open sets.

From b253160353ae89f646ff7fbcff13ca50c4f86cb9 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Sun, 21 Jun 2026 08:59:00 +0200
Subject: [PATCH 12/20] Update properties/P000245.md

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

diff --git a/properties/P000245.md b/properties/P000245.md
index 2e71d4d59..eb7e9984a 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -1,8 +1,6 @@
 ---
 uid: P000245
 name: Has finitely many open sets
-aliases:
-  - Has a finite topology
 ---
 
 $X$ has finitely many open sets.

From 456c1adefe10ba0ee7ca1d450749098dca248cd4 Mon Sep 17 00:00:00 2001
From: Artem <48987557+artemetra@users.noreply.github.com>
Date: Sun, 21 Jun 2026 08:59:23 +0200
Subject: [PATCH 13/20] Update theorems/T000912.md

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

diff --git a/theorems/T000912.md b/theorems/T000912.md
index d820c3d03..9292f988f 100644
--- a/theorems/T000912.md
+++ b/theorems/T000912.md
@@ -8,4 +8,4 @@ then:
   P000078: true
 ---
 
-Follows from the Kolmogorov quotient being finite.
+$\text{Kol}(X)$ is finite, and is equal to $X$ since $X$ is {P1}. So $X$ is finite.

From f2851440fbd682ae167c0fbc645b6eccc38d06e4 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Sun, 21 Jun 2026 14:13:07 +0200
Subject: [PATCH 14/20] generalize t198, t825

---
 theorems/T000198.md | 4 ++--
 theorems/T000825.md | 2 +-
 theorems/T000909.md | 9 ---------
 theorems/T000910.md | 9 ---------
 4 files changed, 3 insertions(+), 21 deletions(-)
 delete mode 100644 theorems/T000909.md
 delete mode 100644 theorems/T000910.md

diff --git a/theorems/T000198.md b/theorems/T000198.md
index 765a4a86e..e71e83b17 100644
--- a/theorems/T000198.md
+++ b/theorems/T000198.md
@@ -1,9 +1,9 @@
 ---
 uid: T000198
 if:
-  P000078: true
+  P000245: true
 then:
   P000208: true
 ---
 
-Finite spaces are compact, and finiteness is a hereditary property.
+Immediate from the definitions.
diff --git a/theorems/T000825.md b/theorems/T000825.md
index ae671e426..6490824f9 100644
--- a/theorems/T000825.md
+++ b/theorems/T000825.md
@@ -1,7 +1,7 @@
 ---
 uid: T000825
 if:
-  P000078: true
+  P000245: true
 then:
   P000226: true
 ---
diff --git a/theorems/T000909.md b/theorems/T000909.md
deleted file mode 100644
index 78e0dd0bb..000000000
--- a/theorems/T000909.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-uid: T000909
-if:
-  P000245: true
-then:
-  P000226: true
----
-
-Immediate from the definitions.
diff --git a/theorems/T000910.md b/theorems/T000910.md
deleted file mode 100644
index 2dfb9cd9f..000000000
--- a/theorems/T000910.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-uid: T000910
-if:
-  P000245: true
-then:
-  P000208: true
----
-
-Immediate from the definitions.

From af3e6ce16e4700f4520111fbc9d97c1f52dc37d7 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Sun, 21 Jun 2026 16:03:20 +0200
Subject: [PATCH 15/20] move theorems

---
 theorems/{T000911.md => T000909.md} | 2 +-
 theorems/{T000912.md => T000910.md} | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename theorems/{T000911.md => T000909.md} (83%)
 rename theorems/{T000912.md => T000910.md} (92%)

diff --git a/theorems/T000911.md b/theorems/T000909.md
similarity index 83%
rename from theorems/T000911.md
rename to theorems/T000909.md
index 61d0dcb10..bdaf52376 100644
--- a/theorems/T000911.md
+++ b/theorems/T000909.md
@@ -1,5 +1,5 @@
 ---
-uid: T000911
+uid: T000909
 if:
   P000129: true
 then:
diff --git a/theorems/T000912.md b/theorems/T000910.md
similarity index 92%
rename from theorems/T000912.md
rename to theorems/T000910.md
index 9292f988f..188673ec7 100644
--- a/theorems/T000912.md
+++ b/theorems/T000910.md
@@ -1,5 +1,5 @@
 ---
-uid: T000912
+uid: T000910
 if:
   and:
     - P000245: true

From dc8df12ce93fca91e4667e9db39a369c3b93718b Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Sun, 21 Jun 2026 21:36:58 -0400
Subject: [PATCH 16/20] Apply suggestion from @prabau

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

diff --git a/properties/P000245.md b/properties/P000245.md
index eb7e9984a..6004eb6c9 100644
--- a/properties/P000245.md
+++ b/properties/P000245.md
@@ -5,7 +5,7 @@ name: Has finitely many open sets
 
 $X$ has finitely many open sets.
 
-Equivalently, the Kolmogorov quotient of the space is finite.
+Equivalently, the Kolmogorov quotient of $X$ is finite.
 
 ----
 #### Meta-properties

From cf60c0341ac1d18fc9c8b08ca839133f81e511fa Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 22 Jun 2026 11:35:49 +0200
Subject: [PATCH 17/20] generalize T251, T658, delete redundant T823

---
 theorems/T000251.md |  2 +-
 theorems/T000658.md |  4 ++--
 theorems/T000823.md | 12 ------------
 3 files changed, 3 insertions(+), 15 deletions(-)
 delete mode 100644 theorems/T000823.md

diff --git a/theorems/T000251.md b/theorems/T000251.md
index eeafd7371..5f6ae496d 100644
--- a/theorems/T000251.md
+++ b/theorems/T000251.md
@@ -1,7 +1,7 @@
 ---
 uid: T000251
 if:
-  P000129: true
+  P000245: true
 then:
   P000016: true
 refs:
diff --git a/theorems/T000658.md b/theorems/T000658.md
index d601a4c6f..c5a86651b 100644
--- a/theorems/T000658.md
+++ b/theorems/T000658.md
@@ -5,7 +5,7 @@ if:
   - P000016: true
   - P000185: true
 then:
-  P000208: true
+  P000245: true
 ---
 
-The ascending chain condition on open sets holds since there are only finitely many open sets.
+The partition generating the topology must be finite due to $X$ being {P16}, so there are only finitely many open sets.
diff --git a/theorems/T000823.md b/theorems/T000823.md
deleted file mode 100644
index bc82ceba9..000000000
--- a/theorems/T000823.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-uid: T000823
-if:
-  and:
-  - P000016: true
-  - P000185: true
-then:
-  P000226: true
----
-
-The partition generating the topology must be finite due to $X$ being {P16}.
-Hence, there can only be finitely many open sets, which trivially implies {P226}.
\ No newline at end of file

From 770ae3c30944810e403b269ecac1e34e2d01e202 Mon Sep 17 00:00:00 2001
From: artemetra <artemlukin15@gmail.com>
Date: Mon, 22 Jun 2026 11:40:54 +0200
Subject: [PATCH 18/20] generalize T189, remove redundant T450

---
 theorems/T000189.md |  4 ++--
 theorems/T000450.md | 12 ------------
 2 files changed, 2 insertions(+), 14 deletions(-)
 delete mode 100644 theorems/T000450.md

diff --git a/theorems/T000189.md b/theorems/T000189.md
index 45ab89a2c..db576c820 100644
--- a/theorems/T000189.md
+++ b/theorems/T000189.md
@@ -1,7 +1,7 @@
 ---
 uid: T000189
 if:
-  P000078: true
+  P000245: true
 then:
   P000027: true
 refs:
@@ -9,7 +9,7 @@ refs:
   name: Counterexamples in Topology
 ---
 
-Space is finite implies the topology is finite, hence countable. Thus the topology itself is a countable basis.
+The topology is finite, hence countable. Thus the topology itself is a countable basis.
 
 Follows directly
 from the definition on page 7 of {{zb:0386.54001}}.
diff --git a/theorems/T000450.md b/theorems/T000450.md
deleted file mode 100644
index 80d61ee8b..000000000
--- a/theorems/T000450.md
+++ /dev/null
@@ -1,12 +0,0 @@
----
-uid: T000450
-if:
-  P000129: true
-then:
-  P000027: true
-refs:
-  - mathse: 3844039
-    name: What topological properties are trivially/vacuously satisfied by any indiscrete space?
----
-
-A space with only finitely many open sets must by definition have a countable basis.

From 3ba02b672bb784e6357d6e283cb72aff0c6f8189 Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Mon, 22 Jun 2026 18:00:24 -0400
Subject: [PATCH 19/20] remove (indiscrete => compact); renumber theorems

---
 theorems/T000189.md | 12 +++---------
 theorems/T000251.md |  9 +++------
 theorems/T000450.md |  9 +++++++++
 theorems/T000908.md |  9 ---------
 theorems/T000909.md |  9 ---------
 5 files changed, 15 insertions(+), 33 deletions(-)
 create mode 100644 theorems/T000450.md
 delete mode 100644 theorems/T000908.md
 delete mode 100644 theorems/T000909.md

diff --git a/theorems/T000189.md b/theorems/T000189.md
index db576c820..2490a9563 100644
--- a/theorems/T000189.md
+++ b/theorems/T000189.md
@@ -1,15 +1,9 @@
 ---
 uid: T000189
 if:
-  P000245: true
+  P000078: true
 then:
-  P000027: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
+  P000245: true
 ---
 
-The topology is finite, hence countable. Thus the topology itself is a countable basis.
-
-Follows directly
-from the definition on page 7 of {{zb:0386.54001}}.
+Immediate from the definition.
diff --git a/theorems/T000251.md b/theorems/T000251.md
index 5f6ae496d..f7ea2a8b6 100644
--- a/theorems/T000251.md
+++ b/theorems/T000251.md
@@ -1,12 +1,9 @@
 ---
 uid: T000251
 if:
-  P000245: true
+  P000129: true
 then:
-  P000016: true
-refs:
-  - mathse: 3844039
-    name: What topological properties are trivially/vacuously satisfied by any indiscrete space?
+  P000245: true
 ---
 
-All open covers are finite to begin with.
+By definition.
diff --git a/theorems/T000450.md b/theorems/T000450.md
new file mode 100644
index 000000000..cdddf1368
--- /dev/null
+++ b/theorems/T000450.md
@@ -0,0 +1,9 @@
+---
+uid: T000450
+if:
+  P000245: true
+then:
+  P000027: true
+---
+
+The topology is finite, hence countable. Thus the topology itself is a countable basis.
diff --git a/theorems/T000908.md b/theorems/T000908.md
deleted file mode 100644
index 485ca4078..000000000
--- a/theorems/T000908.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-uid: T000908
-if:
-  P000078: true
-then:
-  P000245: true
----
-
-Immediate from the definition.
diff --git a/theorems/T000909.md b/theorems/T000909.md
deleted file mode 100644
index bdaf52376..000000000
--- a/theorems/T000909.md
+++ /dev/null
@@ -1,9 +0,0 @@
----
-uid: T000909
-if:
-  P000129: true
-then:
-  P000245: true
----
-
-By definition.

From 9ffc7923ee3d88c6b95317a8b7e8955d0b9b580c Mon Sep 17 00:00:00 2001
From: Patrick Rabau <70125716+prabau@users.noreply.github.com>
Date: Mon, 22 Jun 2026 18:18:44 -0400
Subject: [PATCH 20/20] more renumbering

---
 theorems/{T000910.md => T000823.md} | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename theorems/{T000910.md => T000823.md} (92%)

diff --git a/theorems/T000910.md b/theorems/T000823.md
similarity index 92%
rename from theorems/T000910.md
rename to theorems/T000823.md
index 188673ec7..a719c447d 100644
--- a/theorems/T000910.md
+++ b/theorems/T000823.md
@@ -1,5 +1,5 @@
 ---
-uid: T000910
+uid: T000823
 if:
   and:
     - P000245: true