From 6d9d85e08481ab281ecb316db6570d5e538689a9 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Mon, 1 Sep 2025 02:13:35 +0200 Subject: [PATCH 1/8] added completely uniformizable --- properties/P000221.md | 20 ++++++++++++++++++++ theorems/T000774.md | 9 +++++++++ theorems/T000775.md | 12 ++++++++++++ theorems/T000776.md | 15 +++++++++++++++ 4 files changed, 56 insertions(+) create mode 100644 properties/P000221.md create mode 100644 theorems/T000774.md create mode 100644 theorems/T000775.md create mode 100644 theorems/T000776.md diff --git a/properties/P000221.md b/properties/P000221.md new file mode 100644 index 0000000000..3f12b35316 --- /dev/null +++ b/properties/P000221.md @@ -0,0 +1,20 @@ +--- +uid: P000221 +name: Completely uniformizable +refs: + - wikipedia: Uniform_space + name: Uniform space on Wikipedia + - doi: 10.1007/978-1-4615-7819-2 + name: Rings of Continuous Functions (Gillman & Jerison) +--- + +There exists a complete uniformity on $X$. + +For definition of complete uniformity see . + +Compare with definition in 15.7 of {{doi:10.1007/978-1-4615-7819-2}} where uniform structure is defined using pseudometrics instead. + +---- +#### Meta-properties + +- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does. diff --git a/theorems/T000774.md b/theorems/T000774.md new file mode 100644 index 0000000000..84d37d06e5 --- /dev/null +++ b/theorems/T000774.md @@ -0,0 +1,9 @@ +--- +uid: T000774 +if: + P000221: true +then: + P000012: true +--- + +{P12} spaces are precisely the spaces admitting a uniformity. diff --git a/theorems/T000775.md b/theorems/T000775.md new file mode 100644 index 0000000000..01a7f47b1c --- /dev/null +++ b/theorems/T000775.md @@ -0,0 +1,12 @@ +--- +uid: T000775 +if: + P000162: true +then: + P000221: true +refs: + - doi: 10.1007/978-1-4615-7819-2 + name: Rings of Continuous Functions (Gillman & Jerison) +--- + +See corollary 15.14 of {{doi:10.1007/978-1-4615-7819-2}}. diff --git a/theorems/T000776.md b/theorems/T000776.md new file mode 100644 index 0000000000..2e5b06dd6b --- /dev/null +++ b/theorems/T000776.md @@ -0,0 +1,15 @@ +--- +uid: T000776 +if: + and: + - P000001: true + - P000164: true + - P000221: true +then: + P000162: true +refs: + - doi: 10.1007/978-1-4615-7819-2 + name: Rings of Continuous Functions (Gillman & Jerison) +--- + +A {P221} {P1} space is {P6}. Now apply theorem 15.20 of {{doi:10.1007/978-1-4615-7819-2}}. From 13b6476fe3086b0f3323615e00fcdd706df61bfd Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 00:01:29 +0200 Subject: [PATCH 2/8] added --- properties/P000221.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/properties/P000221.md b/properties/P000221.md index 3f12b35316..9917977c02 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -1,14 +1,19 @@ --- uid: P000221 -name: Completely uniformizable +name: Dieudonné complete +aliases: + - Completely uniformizable + - Topologically complete refs: - wikipedia: Uniform_space name: Uniform space on Wikipedia + - wikipedia: Completely_uniformizable_space + name: Completely uniformizable space - doi: 10.1007/978-1-4615-7819-2 name: Rings of Continuous Functions (Gillman & Jerison) --- -There exists a complete uniformity on $X$. +The topology on the space $X$ is induced by some complete uniformity $\mathcal{U}$. For definition of complete uniformity see . From 6e49252a06cf4def5914f646922630a1ac80336d Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 06:34:30 +0200 Subject: [PATCH 3/8] Kelley --- properties/P000221.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/properties/P000221.md b/properties/P000221.md index 9917977c02..7f22cd8772 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -11,6 +11,8 @@ refs: name: Completely uniformizable space - doi: 10.1007/978-1-4615-7819-2 name: Rings of Continuous Functions (Gillman & Jerison) + - mr: 370454 + name: General Topology (Kelley) --- The topology on the space $X$ is induced by some complete uniformity $\mathcal{U}$. @@ -19,6 +21,8 @@ For definition of complete uniformity see Date: Tue, 2 Sep 2025 07:55:53 +0200 Subject: [PATCH 4/8] added Engelking and equivalent definitions --- properties/P000221.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/properties/P000221.md b/properties/P000221.md index 7f22cd8772..4889733c13 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -13,11 +13,16 @@ refs: name: Rings of Continuous Functions (Gillman & Jerison) - mr: 370454 name: General Topology (Kelley) + - zb: "0684.54001" + name: General Topology (Engelking, 1989) --- -The topology on the space $X$ is induced by some complete uniformity $\mathcal{U}$. +The topology on the space $X$ is induced by a [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness) $\mathcal{U}$. -For definition of complete uniformity see . +If $X$ is $T_0$ this is equivalent to the following (see {{zb:0684.54001}} exercise 8.5.13a): + +2. $X$ is a closed subspace of a product of {P55} spaces +3. $X$ is a closed subspace of a product of {P53} spaces. Compare with definition in 15.7 of {{doi:10.1007/978-1-4615-7819-2}} where uniform structure is defined using pseudometrics instead. From dcf557bbb880ccf517f17a27376daea777d9268f Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 08:01:47 +0200 Subject: [PATCH 5/8] added another justification to a theorem --- theorems/T000775.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theorems/T000775.md b/theorems/T000775.md index 01a7f47b1c..6551d59d05 100644 --- a/theorems/T000775.md +++ b/theorems/T000775.md @@ -9,4 +9,5 @@ refs: name: Rings of Continuous Functions (Gillman & Jerison) --- -See corollary 15.14 of {{doi:10.1007/978-1-4615-7819-2}}. +See corollary 15.14 of {{doi:10.1007/978-1-4615-7819-2}} for complete uniformity on a {P162} space. +Alternatively, a {P162} space is a closed subspace of product of {S25} and {S25|P53}. From a351154e32fef5ec4fe7d76446f100e91a29e04e Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 08:26:29 +0200 Subject: [PATCH 6/8] T386 change --- theorems/T000386.md | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/theorems/T000386.md b/theorems/T000386.md index 2664032d12..6ed386c281 100644 --- a/theorems/T000386.md +++ b/theorems/T000386.md @@ -3,15 +3,9 @@ uid: T000386 if: and: - P000022: true - - P000162: true + - P000221: true then: P000016: true -refs: -- mathse: 4728863 - name: Compactness, pseudocompactness, and realcompactness without Hausdorff --- -Take the space $H\subseteq \mathbb R^\kappa$ (by {P162}); its projection $H_\alpha\subseteq\mathbb R$ -for each factor $\alpha<\kappa$ must be bounded (by {P22}), and thus $\overline{H_\alpha}$ is {P000016} -by the [Heine-Borel theorem](https://en.wikipedia.org/wiki/Heine%E2%80%93Borel_theorem). This makes $H$ -a closed subset of the {P000016} space $\prod_{\alpha<\kappa}\overline{H_\alpha}$, and thus {P000016}. +By taking Kolmogorov quotient we can assume $X$ is $T_0$. If $X\subseteq \prod_\alpha X_\alpha$ is closed where $X_\alpha$ are metric spaces, and $\pi_\alpha:X\to X_\alpha$ is the projection onto $\alpha$th coordinate, then $\pi_\alpha(X)\subseteq X_\alpha$ is {P22} and {P53}, and so {P16}. It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}. From b868adbb2bd595cabd4eaed60d8a516ac53bad22 Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 10:54:40 +0200 Subject: [PATCH 7/8] changes to description, theorem to be finished --- properties/P000221.md | 6 ++++-- theorems/T000777.md | 14 ++++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 theorems/T000777.md diff --git a/properties/P000221.md b/properties/P000221.md index 4889733c13..468c3e83ca 100644 --- a/properties/P000221.md +++ b/properties/P000221.md @@ -19,10 +19,12 @@ refs: The topology on the space $X$ is induced by a [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness) $\mathcal{U}$. +We call uniformity $\mathcal{U}$ complete if every Cauchy filter $\mathcal{F}$ on $(X, \mathcal{U})$ converges. Equivalently, every Cauchy net $(x_i)_{i\in I}$ on $(X, \mathcal{U})$ converges. Here Cauchy filter is a filter $\mathcal{F}$ such that for every $U\in\mathcal{U}$ there exists $A\in\mathcal{F}$ such that $A\times A\subseteq U$. A Cauchy net is a net $(x_i)_{i\in I}$ such that for every $U\in\mathcal{U}$ there exists $i_0$ such that $(x_j, x_k)\in U$ for $j, k\geq i_0$. + If $X$ is $T_0$ this is equivalent to the following (see {{zb:0684.54001}} exercise 8.5.13a): -2. $X$ is a closed subspace of a product of {P55} spaces -3. $X$ is a closed subspace of a product of {P53} spaces. +1. $X$ is a closed subspace of a product of {P55} spaces +2. $X$ is a closed subspace of a product of {P53} spaces. Compare with definition in 15.7 of {{doi:10.1007/978-1-4615-7819-2}} where uniform structure is defined using pseudometrics instead. diff --git a/theorems/T000777.md b/theorems/T000777.md new file mode 100644 index 0000000000..04c6f0a1a9 --- /dev/null +++ b/theorems/T000777.md @@ -0,0 +1,14 @@ +--- +uid: T000777 +if: + and: + - P000134: true + - P000030: true +then: + P000221: true +refs: + - mr: 370454 + name: General Topology (Kelley) +--- + +To be finished. From fb3f3033f07188b2b392ddd2f1743c4648095dac Mon Sep 17 00:00:00 2001 From: Moniker1998 Date: Tue, 2 Sep 2025 11:36:35 +0200 Subject: [PATCH 8/8] proof of T777 updated --- theorems/T000386.md | 2 +- theorems/T000777.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theorems/T000386.md b/theorems/T000386.md index 6ed386c281..ab53aa24d5 100644 --- a/theorems/T000386.md +++ b/theorems/T000386.md @@ -8,4 +8,4 @@ then: P000016: true --- -By taking Kolmogorov quotient we can assume $X$ is $T_0$. If $X\subseteq \prod_\alpha X_\alpha$ is closed where $X_\alpha$ are metric spaces, and $\pi_\alpha:X\to X_\alpha$ is the projection onto $\alpha$th coordinate, then $\pi_\alpha(X)\subseteq X_\alpha$ is {P22} and {P53}, and so {P16}. It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}. +By taking Kolmogorov quotient we can assume $X$ is $T_0$. If $X\subseteq \prod_\alpha X_\alpha$ is closed where $X_\alpha$ are metric spaces, and $\pi_\alpha:X\to X_\alpha$ are projections, then $\pi_\alpha(X)\subseteq X_\alpha$ is {P22} and {P53}, and so {P16}. It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}. diff --git a/theorems/T000777.md b/theorems/T000777.md index 04c6f0a1a9..5f3f9f8d48 100644 --- a/theorems/T000777.md +++ b/theorems/T000777.md @@ -11,4 +11,4 @@ refs: name: General Topology (Kelley) --- -To be finished. +By taking Kolmogorov quotient we can assume $X$ is {P3}. Assume $X$ is not {P221}. Since $X$ is {P207}, the neighbourhoods of the diagonal $\Delta_X\subseteq X\times X$ form a uniformity $\mathcal{U}$ on $X$. Equip $X$ with this uniformity and let $(x_i)_{i\in I}$ be a Cauchy net on $X$ that isn't convergent. Since a Cauchy net converges to each of its adherence points, for each $x\in X$ there exists a neighbourhood $U_x$ of $x$ such that $x_i\notin U_x$ for large enough $i$. From theorem 5.28 of {{mr:370454}}, the open cover $\{U_x : x\in X\}$ is even, so there exists $V\in\mathcal{U}$ such that $V[x] = \{y\in X :(x, y)\in V\}$ is contained in $U_z$ for some $z\in X$. If $i_0$ is such that $(x_j, x_k)\in V$ for $j, k\geq i_0$, then $(x_{i_0}, x_i)\in V$ for all $i\geq i_0$, so $x_i\in V[x_{i_0}]\subseteq U_z$ for all $i\geq i_0$. This is a contradiction since $x_i\notin U_z$ for big enough $i$.