From d331d5ef13c78dc3bd8054e3e7f08c7b7efec7fe Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Wed, 27 May 2026 20:22:22 +0100 Subject: [PATCH 01/15] Add three new theorems, replace T902 because it's made redundant by them --- theorems/T000902.md | 13 +++++++++++-- theorems/T000903.md | 16 ++++++++++++++++ theorems/T000904.md | 15 +++++++++++++++ theorems/T000905.md | 15 +++++++++++++++ 4 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 theorems/T000903.md create mode 100644 theorems/T000904.md create mode 100644 theorems/T000905.md diff --git a/theorems/T000902.md b/theorems/T000902.md index d32fd521d..39e33b8d5 100644 --- a/theorems/T000902.md +++ b/theorems/T000902.md @@ -1,9 +1,18 @@ --- uid: T000902 if: - P000027: true + and: + - P000244: true + - P000026: true then: P000243: true +refs: + - zb: "0559.54003" + name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -A base for the topology is a $\pi$-base. +Let $X = \{x_n: n \in \mathbb{N}\}$ be dense and, for each $p \in X$, $\{V_n(p): n \in \mathbb{N}\}$ be a countable local $\pi$-base for $p$. Then $\{V_n(x_m): n, m \in \mathbb{N}\}$ is a countable (global) $\pi$-base. + +To see this, if $O$ is open, then there is some $m$ so that $x_m \in O$ by hypothesis, and so there is $n$ where $V_n(x_m) \subseteq O$, as desired. + +This is a special case of Theorem 3.8(b) of {{zb:0559.54003}}. diff --git a/theorems/T000903.md b/theorems/T000903.md new file mode 100644 index 000000000..f3f85fb7f --- /dev/null +++ b/theorems/T000903.md @@ -0,0 +1,16 @@ +--- +uid: T000903 +if: + and: + - P000005: true + - P000029: true + - P000191: true + - P000244: true +then: + P000163: true +refs: + - zb: "0559.54003" + name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology +--- + +This is a special case of Corollary 6.4 of {{zb:0559.54003}}. diff --git a/theorems/T000904.md b/theorems/T000904.md new file mode 100644 index 000000000..28efca5b3 --- /dev/null +++ b/theorems/T000904.md @@ -0,0 +1,15 @@ +--- +uid: T000904 +if: + and: + - P000087: true + - P000244: true +then: + P000028: true +--- + +Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\{U_n: n \in \mathbb{N}\}$ be a countable local $\pi$-base around $e$. Put $W_n = \{x \cdot y^{-1}: x, y \in U_n\}$. + +We claim $\{W_n: n \in \mathbb{N}\}$ is a countable local basis around $e$. It is clear that $e \in W_n$. If $O$ is an open neighbourhood of $e$, one can find an open neighbourhood $W$ of $e$ so that $\{x \cdot y: x, y \in W\} \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap \{x^{-1}: x \in W\}$ is open with $e \in V$. + +By hypothesis, there is $n$ so that $U_n \subseteq V$. Then one can easily verify that $W_n \subseteq O$. diff --git a/theorems/T000905.md b/theorems/T000905.md new file mode 100644 index 000000000..47e70c9c0 --- /dev/null +++ b/theorems/T000905.md @@ -0,0 +1,15 @@ +--- +uid: T000905 +if: + and: + - P000003: true + - P000016: true + - P000081: true +then: + P000244: true +refs: + - zb: "0559.54003" + name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology +--- + +This is a special case of Theorem 7.13 of {{zb:0559.54003}}. From a2c74fbb01a09bfe84d3278269f71c89afa4938a Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Thu, 28 May 2026 13:55:35 +0100 Subject: [PATCH 02/15] Update theorems/T000902.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000902.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theorems/T000902.md b/theorems/T000902.md index 39e33b8d5..4315bce0c 100644 --- a/theorems/T000902.md +++ b/theorems/T000902.md @@ -11,8 +11,10 @@ refs: name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -Let $X = \{x_n: n \in \mathbb{N}\}$ be dense and, for each $p \in X$, $\{V_n(p): n \in \mathbb{N}\}$ be a countable local $\pi$-base for $p$. Then $\{V_n(x_m): n, m \in \mathbb{N}\}$ is a countable (global) $\pi$-base. +Let $A$ be a dense subset of $X$. +For each $x\in A$, let $\mathcal V_x$ be a countable local $\pi$-base for $x$. +Then $\bigcup\{\mathcal V_x:x\in A\}$ is a countable (global) $\pi$-base. -To see this, if $O$ is open, then there is some $m$ so that $x_m \in O$ by hypothesis, and so there is $n$ where $V_n(x_m) \subseteq O$, as desired. +To see this, if $O$ is a nonempty open set, there is some $x\in A\cap O$. Hence $O$ contains some $V\in\mathcal V_x$. This is a special case of Theorem 3.8(b) of {{zb:0559.54003}}. From 01dd27212f5cda27e44f2aeedc016a81f53b8619 Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Thu, 28 May 2026 14:14:46 +0100 Subject: [PATCH 03/15] Add metaproperties, simplify T904, optimize hypotheses of T905 --- properties/P000243.md | 2 ++ properties/P000244.md | 2 ++ theorems/T000904.md | 6 +++--- theorems/T000905.md | 2 +- 4 files changed, 8 insertions(+), 4 deletions(-) diff --git a/properties/P000243.md b/properties/P000243.md index 19af65a1c..fd6577c33 100644 --- a/properties/P000243.md +++ b/properties/P000243.md @@ -20,3 +20,5 @@ Defined on page 14 of {{zb:0559.54003}}. #### Meta-properties - This property is hereditary with respect to dense sets. +- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does. +- This property is preserved by countable products. diff --git a/properties/P000244.md b/properties/P000244.md index bf7b1a17c..41088d5c2 100644 --- a/properties/P000244.md +++ b/properties/P000244.md @@ -23,3 +23,5 @@ Defined on page 16 of {{zb:0559.54003}}. #### Meta-properties - This property is hereditary with respect to dense sets. +- $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does. +- This property is preserved by countable products. diff --git a/theorems/T000904.md b/theorems/T000904.md index 28efca5b3..b7f7155d2 100644 --- a/theorems/T000904.md +++ b/theorems/T000904.md @@ -8,8 +8,8 @@ then: P000028: true --- -Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\{U_n: n \in \mathbb{N}\}$ be a countable local $\pi$-base around $e$. Put $W_n = \{x \cdot y^{-1}: x, y \in U_n\}$. +Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\mathcal{U}$ be a countable local $\pi$-base around $e$. Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}. -We claim $\{W_n: n \in \mathbb{N}\}$ is a countable local basis around $e$. It is clear that $e \in W_n$. If $O$ is an open neighbourhood of $e$, one can find an open neighbourhood $W$ of $e$ so that $\{x \cdot y: x, y \in W\} \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap \{x^{-1}: x \in W\}$ is open with $e \in V$. +We claim $\mathcal{W}$ is a countable local basis around $e$. It is clear that every element of $\mathcal{W}$ is a nbhd of $e$. If $O$ is an open nbhd of $e$, one can find an open nbhd $W$ of $e$ so that $W^2 \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap W^{-1}$ is open with $e \in V$. -By hypothesis, there is $n$ so that $U_n \subseteq V$. Then one can easily verify that $W_n \subseteq O$. +By hypothesis, there is $U \in \mathcal{U}$ so that $U \subseteq V$. Then one can easily verify that $U \cdot U^{-1} \subseteq O$. diff --git a/theorems/T000905.md b/theorems/T000905.md index 47e70c9c0..7f903b165 100644 --- a/theorems/T000905.md +++ b/theorems/T000905.md @@ -2,7 +2,7 @@ uid: T000905 if: and: - - P000003: true + - P000134: true - P000016: true - P000081: true then: From a94b8878c8cbdf7b1b0374eb6570a2084ae7b655 Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Thu, 28 May 2026 14:29:28 +0100 Subject: [PATCH 04/15] Add that S108 has P243 since it currently can't be inferred --- spaces/S000108/properties/P000243.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 spaces/S000108/properties/P000243.md diff --git a/spaces/S000108/properties/P000243.md b/spaces/S000108/properties/P000243.md new file mode 100644 index 000000000..44795f072 --- /dev/null +++ b/spaces/S000108/properties/P000243.md @@ -0,0 +1,7 @@ +--- +space: S000108 +property: P000243 +value: true +--- + +The set $\{\{n\}: n < \omega\}$ is a countable $\pi$-base for $\beta \omega$. From 95b66ff03556e6dfdc4cbb94b126b9eeae6aad43 Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Thu, 28 May 2026 18:51:38 +0100 Subject: [PATCH 05/15] Add that S111, S216 have P243 since it currently can't be inferred --- spaces/S000111/properties/P000243.md | 7 +++++++ spaces/S000216/properties/P000243.md | 7 +++++++ 2 files changed, 14 insertions(+) create mode 100644 spaces/S000111/properties/P000243.md create mode 100644 spaces/S000216/properties/P000243.md diff --git a/spaces/S000111/properties/P000243.md b/spaces/S000111/properties/P000243.md new file mode 100644 index 000000000..04e1b0169 --- /dev/null +++ b/spaces/S000111/properties/P000243.md @@ -0,0 +1,7 @@ +--- +space: S000111 +property: P000243 +value: true +--- + +Because {S108|P243} and $X$ is dense in {S108}. diff --git a/spaces/S000216/properties/P000243.md b/spaces/S000216/properties/P000243.md new file mode 100644 index 000000000..c7b53156e --- /dev/null +++ b/spaces/S000216/properties/P000243.md @@ -0,0 +1,7 @@ +--- +space: S000216 +property: P000243 +value: true +--- + +Because {S108|P243} and $X$ is dense in {S108}. From f0aa37e73be0f8697471b72aaabe529c5189297c Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Thu, 28 May 2026 23:14:52 +0100 Subject: [PATCH 06/15] Update spaces/S000111/properties/P000243.md Co-authored-by: Felix Pernegger --- spaces/S000111/properties/P000243.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000111/properties/P000243.md b/spaces/S000111/properties/P000243.md index 04e1b0169..c6a79462b 100644 --- a/spaces/S000111/properties/P000243.md +++ b/spaces/S000111/properties/P000243.md @@ -4,4 +4,4 @@ property: P000243 value: true --- -Because {S108|P243} and $X$ is dense in {S108}. +$X$ is a dense subspace of {S108} and {S108|P243}. From f4c1301fa43fdbc9cd59524006468e998963b421 Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Thu, 28 May 2026 23:15:04 +0100 Subject: [PATCH 07/15] Update spaces/S000216/properties/P000243.md Co-authored-by: Felix Pernegger --- spaces/S000216/properties/P000243.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spaces/S000216/properties/P000243.md b/spaces/S000216/properties/P000243.md index c7b53156e..9bef40420 100644 --- a/spaces/S000216/properties/P000243.md +++ b/spaces/S000216/properties/P000243.md @@ -4,4 +4,4 @@ property: P000243 value: true --- -Because {S108|P243} and $X$ is dense in {S108}. +$X$ is a dense subspace of {S108} and {S108|P243}. From e47b7d00a1467c5b2c0909860ac6cba760603d60 Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Fri, 29 May 2026 09:03:34 +0100 Subject: [PATCH 08/15] Update theorems/T000902.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000902.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000902.md b/theorems/T000902.md index 4315bce0c..a16a29f39 100644 --- a/theorems/T000902.md +++ b/theorems/T000902.md @@ -11,7 +11,7 @@ refs: name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -Let $A$ be a dense subset of $X$. +Let $A$ be a countable dense subset of $X$. For each $x\in A$, let $\mathcal V_x$ be a countable local $\pi$-base for $x$. Then $\bigcup\{\mathcal V_x:x\in A\}$ is a countable (global) $\pi$-base. From de1ec181cf4d000edd9a4ccafaff90b42b6fd3a1 Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Fri, 29 May 2026 09:06:18 +0100 Subject: [PATCH 09/15] Update theorems/T000903.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000903.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000903.md b/theorems/T000903.md index f3f85fb7f..920fef5a9 100644 --- a/theorems/T000903.md +++ b/theorems/T000903.md @@ -2,7 +2,7 @@ uid: T000903 if: and: - - P000005: true + - P000011: true - P000029: true - P000191: true - P000244: true From 1b50e192babcea48dad9f0e7be56d91e872b9c7c Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Fri, 29 May 2026 09:10:37 +0100 Subject: [PATCH 10/15] Update T904 - unabbreviate nbhd & fix typo --- theorems/T000904.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theorems/T000904.md b/theorems/T000904.md index b7f7155d2..8053f077c 100644 --- a/theorems/T000904.md +++ b/theorems/T000904.md @@ -8,8 +8,8 @@ then: P000028: true --- -Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\mathcal{U}$ be a countable local $\pi$-base around $e$. Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}. +Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\mathcal{U}$ be a countable local $\pi$-base around $e$. Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}$. -We claim $\mathcal{W}$ is a countable local basis around $e$. It is clear that every element of $\mathcal{W}$ is a nbhd of $e$. If $O$ is an open nbhd of $e$, one can find an open nbhd $W$ of $e$ so that $W^2 \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap W^{-1}$ is open with $e \in V$. +We claim $\mathcal{W}$ is a countable local basis around $e$. It is clear that every element of $\mathcal{W}$ is a neighbourhood of $e$. If $O$ is an open neighbourhood of $e$, one can find an open neighbourhood $W$ of $e$ so that $W^2 \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap W^{-1}$ is open with $e \in V$. By hypothesis, there is $U \in \mathcal{U}$ so that $U \subseteq V$. Then one can easily verify that $U \cdot U^{-1} \subseteq O$. From 11dbf40f7b34b87a20e82d646726a2c54cd6982e Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Sat, 30 May 2026 18:21:10 +0100 Subject: [PATCH 11/15] Update theorems/T000905.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000905.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theorems/T000905.md b/theorems/T000905.md index 7f903b165..8fbb58907 100644 --- a/theorems/T000905.md +++ b/theorems/T000905.md @@ -12,4 +12,6 @@ refs: name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -This is a special case of Theorem 7.13 of {{zb:0559.54003}}. +The result with {P134} replaced by {P3} is a special case of Theorem 7.13 in {{zb:0559.54003}} +(which uses "compact" to mean compact Hausdorff). +The current result is obtained by passing to the Kolmogorov quotient. From ecd534ea7593aa2addc072eb02cbde65187d7aff Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Sat, 30 May 2026 18:21:56 +0100 Subject: [PATCH 12/15] Update theorems/T000904.md Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com> --- theorems/T000904.md | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/theorems/T000904.md b/theorems/T000904.md index 8053f077c..5a31e6999 100644 --- a/theorems/T000904.md +++ b/theorems/T000904.md @@ -8,8 +8,12 @@ then: P000028: true --- -Because {T347}, it suffices to check the identity element $e$ has a countable local basis. Let $\mathcal{U}$ be a countable local $\pi$-base around $e$. Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}$. +Because {T347}, it suffices to check the identity element $e$ has a countable local base. +Let $\mathcal{U}$ be a countable local $\pi$-base around $e$. +Put $\mathcal{W} = \{U \cdot U^{-1}: U \in \mathcal{U}\}$. -We claim $\mathcal{W}$ is a countable local basis around $e$. It is clear that every element of $\mathcal{W}$ is a neighbourhood of $e$. If $O$ is an open neighbourhood of $e$, one can find an open neighbourhood $W$ of $e$ so that $W^2 \subseteq O$ by continuity of $(x, y) \mapsto x \cdot y$, and then $V = W \cap W^{-1}$ is open with $e \in V$. - -By hypothesis, there is $U \in \mathcal{U}$ so that $U \subseteq V$. Then one can easily verify that $U \cdot U^{-1} \subseteq O$. +We claim $\mathcal{W}$ is a countable local base around $e$. +Every element of $\mathcal{W}$ is an open neighbourhood of $e$. +And if $V$ is a neighbourhood of $e$, there is an open neighbourhood $O$ of $e$ such that $O\cdot O^{-1}\subseteq V$ by continuity of the group operations. +By hypothesis, $O$ contains some $U \in \mathcal{U}$. +Then $U \cdot U^{-1} \subseteq V$. From 3af575e1d440b32ac26b7d668beaf4d9cb01211e Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Sat, 30 May 2026 18:23:51 +0100 Subject: [PATCH 13/15] Update theorems/T000903.md Co-authored-by: Felix Pernegger --- theorems/T000903.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theorems/T000903.md b/theorems/T000903.md index 920fef5a9..a0b90fbef 100644 --- a/theorems/T000903.md +++ b/theorems/T000903.md @@ -13,4 +13,4 @@ refs: name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -This is a special case of Corollary 6.4 of {{zb:0559.54003}}. +See Corollary 6.4 of {{zb:0559.54003}}. From 40522046c1be4a836c328d2486ffab58cc48f812 Mon Sep 17 00:00:00 2001 From: "Jayde :)" <154472391+JSMassmann@users.noreply.github.com> Date: Sat, 30 May 2026 18:24:24 +0100 Subject: [PATCH 14/15] Remove evidently unintentional newline --- theorems/T000905.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theorems/T000905.md b/theorems/T000905.md index 8fbb58907..435731b5e 100644 --- a/theorems/T000905.md +++ b/theorems/T000905.md @@ -12,6 +12,5 @@ refs: name: Cardinal functions I (R. Hodel), Ch. 1 of Handbook of set-theoretic topology --- -The result with {P134} replaced by {P3} is a special case of Theorem 7.13 in {{zb:0559.54003}} -(which uses "compact" to mean compact Hausdorff). +The result with {P134} replaced by {P3} is a special case of Theorem 7.13 in {{zb:0559.54003}} (which uses "compact" to mean compact Hausdorff). The current result is obtained by passing to the Kolmogorov quotient. From b6a616b05a6ddbcdcbdc2ef00136b2b3c05fdc0b Mon Sep 17 00:00:00 2001 From: JSMassmann Date: Sun, 31 May 2026 11:41:58 +0100 Subject: [PATCH 15/15] Add open metaproperty --- properties/P000243.md | 1 + properties/P000244.md | 1 + 2 files changed, 2 insertions(+) diff --git a/properties/P000243.md b/properties/P000243.md index fd6577c33..975cb6e24 100644 --- a/properties/P000243.md +++ b/properties/P000243.md @@ -20,5 +20,6 @@ Defined on page 14 of {{zb:0559.54003}}. #### Meta-properties - This property is hereditary with respect to dense sets. +- This property is hereditary with respect to open sets. - $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does. - This property is preserved by countable products. diff --git a/properties/P000244.md b/properties/P000244.md index 41088d5c2..bd7408392 100644 --- a/properties/P000244.md +++ b/properties/P000244.md @@ -23,5 +23,6 @@ Defined on page 16 of {{zb:0559.54003}}. #### Meta-properties - This property is hereditary with respect to dense sets. +- This property is hereditary with respect to open sets. - $X$ satisfies this property iff its Kolmogorov quotient $\operatorname{Kol}(X)$ does. - This property is preserved by countable products.