Simple theorems for Artinian (P226)

properties/P000226.md

@@ -4,18 +4,24 @@ name: Artinian
 refs:
   - zb: "0392.54005"
     name: Finite $T_0$-spaces and universal mappings. (Holsztyński, Pedersen)
+  - mathse: 5117935
+    name: Equivalent definitions of an Artinian space
 ---
 
-A space for which every collection of open sets has a minimal element.
+Every nonempty collection of open sets has a minimal element.
 
 Equivalently:
-- Every collection of closed sets has a maximal element.
+- Every nonempty collection of closed sets has a maximal element.
 - The open sets satisfy the *descending chain condition*: There is no infinite strictly decreasing sequence $O_1 \supsetneq O_2 \supsetneq \cdots$ of open sets.
 - The closed sets satisfy the *ascending chain condition*: There is no infinite strictly increasing sequence $Y_1 \subsetneq Y_2 \subsetneq \cdots$ of closed sets.
+- Every subspace has a finite dense subset.
 
-See Section 1 of {{zb:0392.54005}}.
+See {{mathse:5117935}} for a proof of the equivalences.
+
+Compare with {P208}.
 
 ----
 #### Meta-properties
 
 - This property is hereditary.
+- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.

theorems/T000823.md

@@ -1,9 +1,12 @@
 ---
 uid: T000823
 if:
-  P000129: true
+  and:
+  - P000016: true
+  - P000185: true
 then:
   P000226: true
 ---
 
-All collections of open sets are finite.
+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}.

theorems/T000824.md

@@ -2,10 +2,10 @@
 uid: T000824
 if:
   and:
-  - P000078: false
+  - P000226: true
   - P000002: true
 then:
-  P000226: false
+  P000078: true
 ---
 
-Pick distinct $x_1,x_2,\dots\in X$. Then $\{x_1\}\subsetneq \{x_1,x_2\}\subsetneq\{x_1, x_2, x_3\} \subsetneq \dots$ is an infinite ascending chain of closed subsets.
+Since $X$ is {P226}, we can find a finite dense set $F\subseteq X$. Since $X$ is {P2}, $F$ is closed, so $F = X$.

theorems/T000827.md

@@ -0,0 +1,14 @@
+---
+uid: T000827
+if:
+  and:
+  - P000226: true
+  - P000203: true
+then:
+  P000078: true
+---
+
+Let $p \in X$ be the non-isolated point.
+Then $X\setminus\{p\}$ is {P52} and {P226},
+hence {P78}
+[(Explore)](https://topology.pi-base.org/spaces?q=Discrete%2BArtinian%2B%7EFinite).

theorems/T000828.md

@@ -0,0 +1,10 @@
+---
+uid: T000828
+if:
+  P000226: true
+then:
+  P000021: true
+---
+
+Since {P226} is hereditary, every discrete subset of $X$ is finite
+[(Explore)](https://topology.pi-base.org/spaces?q=Discrete%2BArtinian%2B%7EFinite).

theorems/T000829.md

@@ -0,0 +1,14 @@
+---
+uid: T000829
+if:
+  and:
+  - P000226: true
+  - P000045: true
+then:
+  P000078: true
+---
+
+Let $p\in X$ be the dispersion point.
+Then $X\setminus\{p\}$ is {P226} and {P47},
+hence {P78}
+[(Explore)](https://topology.pi-base.org/spaces?q=Totally+disconnected%2BArtinian%2B%7EFinite).

theorems/T000830.md

@@ -0,0 +1,11 @@
+---
+uid: T000830
+if:
+  and:
+  - P000226: true
+  - P000185: true
+then:
+  P000016: true
+---
+
+If $X$ is a {P185}, then $X$ is {P16} iff the Kolmogorov quotient $\text{Kol}(X)$ is finite. The assertion then follows from {T824}.

theorems/T000831.md

@@ -0,0 +1,16 @@
+---
+uid: T000831
+if:
+  and:
+  - P000226: true
+  - P000001: true
+then:
+  P000051: true
+---
+
+Let $A$ be a nonempty subset of $X$.
+Let $U$ be a minimal open set in $X$ with $U\cap A\ne\emptyset$.
+The set $U\cap A$ cannot contain two distinct points;
+otherwise, by the {P1} property there would be an open set $V$ in $X$ containing one point and not the other.
+Then $U\cap V$ would be a strictly smaller open set that meets $A$, which is not possible.
+Thus, the element of $U\cap A$ is isolated in $A$.

theorems/T000832.md

@@ -0,0 +1,9 @@
+---
+uid: T000832
+if:
+  P000226: true
+then:
+  P000180: true
+---
+
+Immediate from the definitions.