From 5603939d7012afc792114fc87eb0798ded22bfef Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Thu, 23 Jul 2026 04:36:05 +0200 Subject: [PATCH 1/9] submetrizable implies D. complete --- theorems/T000918.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 theorems/T000918.md diff --git a/theorems/T000918.md b/theorems/T000918.md new file mode 100644 index 000000000..d0787c540 --- /dev/null +++ b/theorems/T000918.md @@ -0,0 +1,14 @@ +--- +uid: T000918 +if: + and: + - P000012: true + - P000112: true +then: + P000221: true +refs: + - zb: "1380.46022" + name: Rings of Continuous Functions (Gillman & Jerison) +--- + +See exercise 15U.3 of {{zb:1380.46022}}. From 27240c25142920c2ff08752b88508418f447c7f0 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Thu, 23 Jul 2026 05:49:37 +0200 Subject: [PATCH 2/9] re-numbered --- theorems/{T000918.md => T000923.md} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename theorems/{T000918.md => T000923.md} (94%) diff --git a/theorems/T000918.md b/theorems/T000923.md similarity index 94% rename from theorems/T000918.md rename to theorems/T000923.md index d0787c540..bfc867f55 100644 --- a/theorems/T000918.md +++ b/theorems/T000923.md @@ -1,5 +1,5 @@ --- -uid: T000918 +uid: T000923 if: and: - P000012: true From 0ea8d478514bb7bf03511db5e1d04908c3949cf8 Mon Sep 17 00:00:00 2001 From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com> Date: Fri, 24 Jul 2026 05:56:40 +0200 Subject: [PATCH 3/9] Update T000923.md --- theorems/T000923.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theorems/T000923.md b/theorems/T000923.md index bfc867f55..404cc49b3 100644 --- a/theorems/T000923.md +++ b/theorems/T000923.md @@ -11,4 +11,6 @@ refs: name: Rings of Continuous Functions (Gillman & Jerison) --- -See exercise 15U.3 of {{zb:1380.46022}}. +See 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}. From 20caa399692a5b95160417bc76c22f157c40e104 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Fri, 24 Jul 2026 06:02:03 +0200 Subject: [PATCH 4/9] connected realcompact and Dieudonne complete --- properties/P000162.md | 3 +++ properties/P000221.md | 3 +++ 2 files changed, 6 insertions(+) diff --git a/properties/P000162.md b/properties/P000162.md index 5ec4567f0..5abf53eb1 100644 --- a/properties/P000162.md +++ b/properties/P000162.md @@ -18,3 +18,6 @@ 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}}. + +From {T915} and {T916}, it follows that if a space is {P164}, +then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. diff --git a/properties/P000221.md b/properties/P000221.md index be383c61f..53ebfff7c 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -36,6 +36,9 @@ 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}. +From {T915} and {T916}, it follows that if a space is {P164}, +then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. + ---- #### Meta-properties From f186ca3d323e13d82a745554b43130dd2528c9df Mon Sep 17 00:00:00 2001 From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com> Date: Fri, 24 Jul 2026 10:01:22 +0200 Subject: [PATCH 5/9] Update theorems/T000923.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000923.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000923.md b/theorems/T000923.md index 404cc49b3..48a40c290 100644 --- a/theorems/T000923.md +++ b/theorems/T000923.md @@ -2,8 +2,8 @@ uid: T000923 if: and: - - P000012: true - P000112: true + - P000006: true then: P000221: true refs: From 7eb153aafc8da06b549a77cbfe40c55c0d277e94 Mon Sep 17 00:00:00 2001 From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com> Date: Fri, 24 Jul 2026 10:02:26 +0200 Subject: [PATCH 6/9] Update properties/P000162.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- properties/P000162.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/properties/P000162.md b/properties/P000162.md index 5abf53eb1..608bf549a 100644 --- a/properties/P000162.md +++ b/properties/P000162.md @@ -19,5 +19,4 @@ A *$z$-ultrafilter* is an ultrafilter on the lattice of zero-sets of $X$ (see {{ See also section 3.11 in {{zb:0684.54001}}. -From {T915} and {T916}, it follows that if a space is {P164}, -then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. +Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. From 63910318f4aceab509d573ff833a463f35b6cc08 Mon Sep 17 00:00:00 2001 From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com> Date: Fri, 24 Jul 2026 10:04:17 +0200 Subject: [PATCH 7/9] Update P000221.md --- properties/P000221.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/properties/P000221.md b/properties/P000221.md index 53ebfff7c..69d5c6e35 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -36,8 +36,7 @@ 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}. -From {T915} and {T916}, it follows that if a space is {P164}, -then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. +Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}. ---- #### Meta-properties From c9b53fba9078ba081c2c26b1d3bb3c2e44f18ea9 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Thu, 30 Jul 2026 13:00:55 +0200 Subject: [PATCH 8/9] added reference --- theorems/T000923.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theorems/T000923.md b/theorems/T000923.md index 48a40c290..f171625ad 100644 --- a/theorems/T000923.md +++ b/theorems/T000923.md @@ -9,8 +9,10 @@ then: refs: - zb: "1380.46022" name: Rings of Continuous Functions (Gillman & Jerison) + - zb: "1323.22001" + name: Topological groups and related structures (Arhangel’skii, Tkachenko) --- -See exercise 15U.3 of {{zb:1380.46022}}. +See theorem 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}. From 428d3fda207fcd43c687e67a533dc8c421bae2a7 Mon Sep 17 00:00:00 2001 From: Moniker1998 <88507423+Moniker1998@users.noreply.github.com> Date: Thu, 30 Jul 2026 13:02:27 +0200 Subject: [PATCH 9/9] Update T000923.md --- theorems/T000923.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000923.md b/theorems/T000923.md index f171625ad..27b9513e7 100644 --- a/theorems/T000923.md +++ b/theorems/T000923.md @@ -13,6 +13,6 @@ refs: name: Topological groups and related structures (Arhangel’skii, Tkachenko) --- -See theorem 6.10.8 of {{zb:1323.22001} and exercise 15U.3 of {{zb:1380.46022}}. +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}.