Finite topology property + simple theorems

properties/P000245.md

@@ -0,0 +1,16 @@
+---
+uid: P000245
+name: Has finitely many open sets
+---
+
+$X$ has finitely many open sets.
+
+Equivalently, the Kolmogorov quotient of $X$ is finite.
+
+----
+#### Meta-properties
+
+- This property is hereditary.
+- This property is preserved in any coarser topology.
+- $X$ is {P245} iff its Kolmogorov quotient $\text{Kol}(X)$ is {P78}.
+- This property is preserved by finite products.

theorems/T000189.md

@@ -3,13 +3,7 @@ uid: T000189
 if:
   P000078: true
 then:
-  P000027: true
-refs:
-- zb: "0386.54001"
-  name: Counterexamples in Topology
+  P000245: true
 ---
 
-Space is finite implies 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.

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.

theorems/T000251.md

@@ -3,10 +3,7 @@ uid: T000251
 if:
   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.

theorems/T000450.md

@@ -1,12 +1,9 @@
 ---
 uid: T000450
 if:
-  P000129: true
+  P000245: 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.
+The topology is finite, hence countable. Thus the topology itself is a countable basis.

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.

theorems/T000823.md

@@ -2,11 +2,10 @@
 uid: T000823
 if:
   and:
-  - P000016: true
-  - P000185: true
+    - P000245: true
+    - P000001: true
 then:
-  P000226: true
+  P000078: 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}.
+$\text{Kol}(X)$ is finite, and is equal to $X$ since $X$ is {P1}. So $X$ is finite.

theorems/T000825.md

@@ -1,7 +1,7 @@
 ---
 uid: T000825
 if:
-  P000078: true
+  P000245: true
 then:
   P000226: true
 ---