pi-base · felixpernegger · Jul 31, 2026 · Jul 23, 2026 · Jul 23, 2026 · Jul 24, 2026
diff --git a/properties/P000162.md b/properties/P000162.md
@@ -18,3 +18,5 @@ that is, $\bigcap\mathcal{U}\neq\emptyset$.
 A *$z$-ultrafilter* is an ultrafilter on the lattice of zero-sets of $X$ (see {{wikipedia:Ultrafilter}} for the general definition of an ultrafilter on a poset). A *real $z$-ultrafilter* is a $z$-ultrafilter with countable intersection property, that is, for any countable $\mathcal{F}\subseteq \mathcal{U}$ we have $\bigcap\mathcal{F}\neq \emptyset$.
 
 See also section 3.11 in {{zb:0684.54001}}.
+
+Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
diff --git a/properties/P000221.md b/properties/P000221.md
@@ -36,6 +36,8 @@ Such spaces are called *Dieudonné complete* (Problem 8.5.13 in {{zb:0684.54001}
 They are called *topologically complete* on page 208 of {{mr:370454}}; 
 this last term has also been used for {P55} and {P63}.
 
+Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
+
 ----
 #### Meta-properties
 

diff --git a/theorems/T000923.md b/theorems/T000923.md
@@ -0,0 +1,18 @@
+---
+uid: T000923
+if:
+  and:
+  - P000112: true
+  - P000006: true
+then:
+  P000221: true
+refs:
+  - zb: "1380.46022"
+    name: Rings of Continuous Functions (Gillman & Jerison)
+  - zb: "1323.22001"
+    name: Topological groups and related structures (Arhangel’skii, Tkachenko)
+---
+
+See proposition 6.10.8 of {{zb:1323.22001} and exercise 15U.3 of {{zb:1380.46022}}. 
+
+*Remark.* Note that since {P112} is a hereditary property, it follows that the space is hereditarily {P221}. This improves {T742}.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -18,3 +18,5 @@ that is, $\bigcap\mathcal{U}\neq\emptyset$.
		A $z$-ultrafilter is an ultrafilter on the lattice of zero-sets of $X$ (see {{wikipedia:Ultrafilter}} for the general definition of an ultrafilter on a poset). A real $z$-ultrafilter is a $z$-ultrafilter with countable intersection property, that is, for any countable $\mathcal{F}\subseteq \mathcal{U}$ we have $\bigcap\mathcal{F}\neq \emptyset$.

		See also section 3.11 in {{zb:0684.54001}}.

		Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
felixpernegger Jul 29, 2026 Copy link Copy Markdown Collaborator Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. This is more about P221 than about P162, so I would delete this sentence here prabau Jul 30, 2026 Copy link Copy Markdown Collaborator Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. I think this sentence is useful and worth keeping. It basically says (implies) that for T0 spaces with reasonable cardinality, realcompact and Dieudonne complete are equivalent properties. Moniker1998 Jul 30, 2026 Copy link Copy Markdown Collaborator Author Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. @felixpernegger what do you mean?