Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
6d9d85e
added completely uniformizable
Moniker1998 Sep 1, 2025
13b6476
added
Moniker1998 Sep 1, 2025
6e49252
Kelley
Moniker1998 Sep 2, 2025
923600b
added Engelking and equivalent definitions
Moniker1998 Sep 2, 2025
dcf557b
added another justification to a theorem
Moniker1998 Sep 2, 2025
a351154
T386 change
Moniker1998 Sep 2, 2025
b868adb
changes to description, theorem to be finished
Moniker1998 Sep 2, 2025
fb3f303
proof of T777 updated
Moniker1998 Sep 2, 2025
1fe2b16
Update properties/P000221.md
Moniker1998 Jul 12, 2026
95c5c37
Apply suggestion from @prabau
Moniker1998 Jul 12, 2026
e9168d0
Update P000221.md
Moniker1998 Jul 12, 2026
0f93f37
Update P000221.md
Moniker1998 Jul 12, 2026
266fc1e
Update T000386.md
Moniker1998 Jul 12, 2026
9fd4fe0
add Kolmogorov meta to P22
Moniker1998 Jul 12, 2026
fe75d38
add explore link to T777
Moniker1998 Jul 12, 2026
cec9bf6
add note to P207
Moniker1998 Jul 12, 2026
23ebe1c
added a remark that uniformity induces topology
Moniker1998 Jul 12, 2026
f9d4d2c
add explore to T776
Moniker1998 Jul 12, 2026
ecb2f1a
Update theorems/T000777.md
Moniker1998 Jul 12, 2026
5fd2db6
Cauchy net converges to its adherence points
Moniker1998 Jul 13, 2026
b496e50
Update T000777.md
Moniker1998 Jul 13, 2026
50036a8
fix a broken file
Moniker1998 Jul 13, 2026
3c2a191
T777: remove duplicate text, plus cosmetic changes
prabau Jul 13, 2026
11dd212
fix missing double quotes
prabau Jul 13, 2026
60f4995
Update theorems/T000777.md
Moniker1998 Jul 14, 2026
710c326
elaboration on nomenclature
Moniker1998 Jul 14, 2026
99ed32e
rephrased equivalent statements to include non-T0 case
Moniker1998 Jul 14, 2026
d3b077d
renamed theorems
Moniker1998 Jul 16, 2026
d75a5b1
Merge branch 'main' into completely-uniformizable
Moniker1998 Jul 16, 2026
7d964f8
doi => zb
felixpernegger Jul 16, 2026
f26685d
P63 cosmetic
prabau Jul 17, 2026
9517dd6
P221 updates
prabau Jul 17, 2026
ed83bb5
Update properties/P000055.md
Moniker1998 Jul 17, 2026
5f9e3d1
T915 cosmetic
prabau Jul 18, 2026
d94dcda
Update theorems/T000917.md
Moniker1998 Jul 20, 2026
eaffea7
Update theorems/T000917.md
Moniker1998 Jul 20, 2026
a95d2c5
Update properties/P000221.md
Moniker1998 Jul 20, 2026
09b8ea2
Update theorems/T000916.md
Moniker1998 Jul 20, 2026
070ab95
Update theorems/T000386.md
Moniker1998 Jul 20, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions properties/P000022.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,5 @@ Defined on page 20 of {{zb:0386.54001}}.
----
#### Meta-properties

- $X$ satisfies this property iff its Kolmogorov quotient $\mathrm{Kol}(X)$ does.
- This property is preserved in any coarser topology.
4 changes: 2 additions & 2 deletions properties/P000049.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ name: Extremally disconnected
refs:
- zb: "1052.54001"
name: General Topology (Willard)
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
- zb: "0386.54001"
name: Counterexamples in Topology
Expand All @@ -18,7 +18,7 @@ The closure of every open set in $X$ is open or, equivalently, clopen.

Equivalently, any two disjoint open sets have disjoint closures.

Defined in problem 15G of {{zb:1052.54001}} and problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
Defined in problem 15G of {{zb:1052.54001}} and problem 1H of {{zb:1380.46022}}.

{{zb:0386.54001}} defines it on page 32 with the additional assumption of {P3},
which we do not assume here.
Expand Down
5 changes: 3 additions & 2 deletions properties/P000055.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,9 @@ that is, a metric for which every Cauchy sequence converges.
A sequence $(x_n)_n$ is *Cauchy* provided for each distance $\epsilon>0$, there is
a natural number $N$ for which $d(x_i,x_j)<\epsilon$ for all $i,j>N$.

See Definition 24.2 in {{zb:1052.54001}}.
Defined on page 37 of {{zb:0386.54001}} as "topologically complete".
Defined in 24.2 of {{zb:1052.54001}}.
Called *topologically complete* on page 37 of {{zb:0386.54001}};
this last term has also been used for {P63} and {P221}.

----
#### Meta-properties
Expand Down
9 changes: 8 additions & 1 deletion properties/P000063.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,22 @@
---
uid: P000063
name: Čech complete
aliases:
- Topologically complete
refs:
- zb: "0684.54001"
name: General Topology (Engelking, 1989)
- zb: "0117.15903"
name: A characterization of topologically complete spaces in the sense of E. Čech in terms of convergence of functions. (Frolik, 1963)
---
A {P6} space $X$ that is a $G_\delta$ set in some compactification of $X$ (equivalently, in every compactification of $X$).

Equivalently, there is a sequence $\mathcal{U}_1, \mathcal{U}_2, \dots$ of open covers of $X$ such that whenever $\mathcal{F}$ is a family of closed sets with the finite intersection property and such that for each $n$ there is some $F_n \in \mathcal{F}$ with $F_n \subseteq U$ for some $U \in \mathcal{U}_n$, then $\bigcap \mathcal F \neq \emptyset$.

See Section 3.9 of {{zb:0684.54001}}, specifically Theorems 3.9.1 and 3.9.2 for the equivalences above.
See Section 3.9 ("Čech-complete spaces") of {{zb:0684.54001}}, specifically Theorems 3.9.1 and 3.9.2 for the equivalences above.

Such spaces are called *topologically complete* in {{zb:0117.15903}};
this last term has also been used for {P55} and {P221}.

----
#### Meta-properties
Expand Down
4 changes: 2 additions & 2 deletions properties/P000085.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
uid: P000085
name: Basically disconnected
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

Expand All @@ -13,7 +13,7 @@ equivalently, the complement of a zero set.

Equivalently, any two disjoint open sets, at least one of which is a cozero set, have disjoint closures.

Defined in problem 1H of {{doi:10.1007/978-1-4615-7819-2}}.
Defined in problem 1H of {{zb:1380.46022}}.

No additional separation axiom is assumed here.

Expand Down
4 changes: 2 additions & 2 deletions properties/P000162.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,15 @@ name: Realcompact
refs:
- zb: "0684.54001"
name: General Topology (Engelking, 1989)
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
- wikipedia: Ultrafilter
name: Ultrafilter on Wikipedia
---

A space $X$ that is homeomorphic to a closed subset of $\mathbb{R}^\kappa$ for some cardinal $\kappa$.

Equivalently (see {{doi:10.1007/978-1-4615-7819-2}}), $X$ is {P6} and every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
Equivalently (see {{zb:1380.46022}}), $X$ is {P6} and every real $z$-ultrafilter $\mathcal U$ on the space $X$ is fixed,
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$.
Expand Down
4 changes: 2 additions & 2 deletions properties/P000164.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ aliases:
refs:
- wikipedia: Measurable_cardinal
name: Measurable cardinal on Wikipedia
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
- doi: 10.1007/3-540-44761-X
name: Set Theory (Jech)
Expand All @@ -22,7 +22,7 @@ A cardinal $\kappa$ is called *measurable* if $\kappa$ is uncountable and there

Equivalently, $\kappa$ is uncountable and there exists a free ultrafilter $\mathcal{U}$ on $\kappa$ such that $\mathcal{U}$ is *$\kappa$-complete*, i.e., if $\mathcal{F}\subseteq \mathcal{U}$ and $|\mathcal{F}| < \kappa$ then $\bigcap\mathcal{F}\in \mathcal{U}$. (See {{wikipedia:Measurable_cardinal}} for more details.)

Note: Some authors, for example {{doi:10.1007/978-1-4615-7819-2}}, refer to measurable cardinals as those cardinals $\kappa$ for which there exists a $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ which is non-trivial. If $\kappa$ is the smallest such cardinal, then a non-trivial $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ is $\kappa$-additive (see lemma 10.2 of {{doi:10.1007/3-540-44761-X}} and comments preceding it), so $\kappa$ is also measurable by the above definition.
Note: Some authors, for example {{zb:1380.46022}}, refer to measurable cardinals as those cardinals $\kappa$ for which there exists a $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ which is non-trivial. If $\kappa$ is the smallest such cardinal, then a non-trivial $\sigma$-additive measure $\mu:2^\kappa\to \{0, 1\}$ is $\kappa$-additive (see lemma 10.2 of {{doi:10.1007/3-540-44761-X}} and comments preceding it), so $\kappa$ is also measurable by the above definition.

(The existence of a measurable cardinal cannot be proven in ZFC.
So spaces whose construction does not depend on set-theoretic axioms beyond ZFC should never have this property marked as false.)
Expand Down
2 changes: 2 additions & 0 deletions properties/P000207.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ For each neighborhood $U$ of the diagonal $\Delta=\{(x,x)\mid x\in X\}$
in $X\times X$, there is a neighborhood $V$ of the diagonal such that
$V\circ V\subseteq U$.

This is equivalent to the family $\mathcal{U}$ of neighborhoods of $\Delta_X$ forming a uniformity, but the topology of $X$ and that of $(X, \mathcal{U})$ do not need to agree. If $X$ is {P12} then both topologies coincide.

In Theorem 2.6 of {{doi:10.2307/1993026}} this property was shown to be equivalent to
*almost $2$-fully normal*: each open cover $\mathcal U$ has an open almost $2$-star
refinement $\mathcal V$, that is $\mathcal{V}$ is a refinement of $\mathcal{U}$ and for any $x, y, z$ with $y, z\in \text{St}(x, \mathcal{V})$ there exists $U\in\mathcal{U}$ with $y, z\in U$.
Expand Down
4 changes: 2 additions & 2 deletions properties/P000215.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@
uid: P000215
name: Hereditarily realcompact
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

Every subspace is {P162}.

Equivalently, $X$ is {P6} and $X\setminus \{x\}$ is realcompact for each $x\in X$. (theorem 8.17 of {{doi:10.1007/978-1-4615-7819-2}})
Equivalently, $X$ is {P6} and $X\setminus \{x\}$ is realcompact for each $x\in X$. (theorem 8.17 of {{zb:1380.46022}})

----
#### Meta-properties
Expand Down
44 changes: 44 additions & 0 deletions properties/P000221.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
---
uid: P000221
name: Dieudonné complete
aliases:
- Completely uniformizable
- Topologically complete
refs:
- wikipedia: Completely_uniformizable_space
name: Completely uniformizable space
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
- mr: 370454
name: General Topology (Kelley)
- zb: "0684.54001"
name: General Topology (Engelking, 1989)
- zb: "1052.54001"
name: General Topology (Willard, 1970)
- zb: "0024.36301"
name: Sur les espaces uniformes complets (Dieudonné)
---

There exists at least one [complete uniformity](https://en.wikipedia.org/wiki/Uniform_space#Completeness)
that induces the topology of $X$.

This is equivalent to each of the following:
- $X$ is homeomorphic to a closed subspace of a product of completely pseudometrizable spaces.
- $X$ is homeomorphic to a closed subspace of a product of {P121} spaces.

For the equivalence, see Problem 8.5.13(z) in {{zb:0684.54001}} and page 285 of {{zb:0024.36301}}.

Terminology:
We call a 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 a *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$.
(Compare with the definition of complete uniformity in 15.7 of {{zb:1380.46022}} where uniform structure is defined using pseudometrics.)

Such spaces are called *Dieudonné complete* (Problem 8.5.13 in {{zb:0684.54001}}) or *completely uniformizable* (Problem 39B in {{zb:1052.54001}}).
They are called *topologically complete* on page 208 of {{mr:370454}};
this last term has also been used for {P55} and {P63}.

----
#### Meta-properties

- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
- This property is preserved by arbitrary products.
- This property is hereditary with respect to closed sets.
4 changes: 2 additions & 2 deletions spaces/S000074/properties/P000162.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ space: S000074
property: P000162
value: true
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
---

The identity function $\text{Id}:X\to \mathbb{R}^2$, $\text{Id}(x) = x$ from {S74} to {S176} is a continuous injection. Since every subspace of {S176} is realcompact ({S176} is {P5} and {P131}, and see {T384}), {S74} is realcompact from corollary 8.18 in {{doi:10.1007/978-1-4615-7819-2}}.
The identity function $\text{Id}:X\to \mathbb{R}^2$, $\text{Id}(x) = x$ from {S74} to {S176} is a continuous injection. Since every subspace of {S176} is realcompact ({S176} is {P5} and {P131}, and see {T384}), {S74} is realcompact from corollary 8.18 in {{zb:1380.46022}}.
4 changes: 2 additions & 2 deletions spaces/S000107/properties/P000162.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ space: S000107
property: P000162
value: true
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
---

The identity function $\text{Id}:\mathbb{R}^\omega\to \mathbb{R}^\omega$, $\text{Id}(x) = x$ from {S107} to $\mathbb{R}^\omega$ with product topology is a continuous bijection. Since every subspace of $\mathbb{R}^\omega$ with product topology is realcompact ($\mathbb{R}^\omega$ is {P5} and {P131}, and see {T384}), {S107} is realcompact from corollary 8.18 in {{doi:10.1007/978-1-4615-7819-2}}.
The identity function $\text{Id}:\mathbb{R}^\omega\to \mathbb{R}^\omega$, $\text{Id}(x) = x$ from {S107} to $\mathbb{R}^\omega$ with product topology is a continuous bijection. Since every subspace of $\mathbb{R}^\omega$ with product topology is realcompact ($\mathbb{R}^\omega$ is {P5} and {P131}, and see {T384}), {S107} is realcompact from corollary 8.18 in {{zb:1380.46022}}.

4 changes: 2 additions & 2 deletions spaces/S000153/properties/P000162.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ space: S000153
property: P000162
value: false
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
---

The subspace $X\subseteq Y$ of {S153} given by $X = \{(x, 0) : 0 < x < \omega_1\}$ is a closed copy of $\omega_1$ in $Y$. If $Y$ were realcompact, then its closed subspace $X$ would be realcompact (see theorem 8.10 in {{doi:10.1007/978-1-4615-7819-2}}). But $\omega_1$ is a pseudocompact non-compact Tychonoff space, so is not realcompact, see {T388}.
The subspace $X\subseteq Y$ of {S153} given by $X = \{(x, 0) : 0 < x < \omega_1\}$ is a closed copy of $\omega_1$ in $Y$. If $Y$ were realcompact, then its closed subspace $X$ would be realcompact (see theorem 8.10 in {{zb:1380.46022}}). But $\omega_1$ is a pseudocompact non-compact Tychonoff space, so is not realcompact, see {T388}.
4 changes: 2 additions & 2 deletions spaces/S000208/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ name: Hewitt realcompactification of Rudin's Dowker space
refs:
- zb: "0224.54019"
name: A normal space X for which X×I is not normal (M.E. Rudin)
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
- wikipedia: Cofinality#Cofinality_of_ordinals_and_other_well-ordered_sets
name: Cofinality on Wikipedia
Expand All @@ -13,4 +13,4 @@ refs:
$X$ is the subspace of the product $\prod_{n\in\omega}(\omega_{n+1}+1)$ with the box topology consisting of all $f\in \prod_{n\in \omega}(\omega_{n+1}+1)$ such that $\omega< \text{cf}(f(n))$ for all $n$ (see {{wikipedia:Cofinality#Cofinality_of_ordinals_and_other_well-ordered_sets}}).

Defined (as the space called $X'$) and shown to be the Hewitt realcompactification of {S138} in section IV.4 of {{zb:0224.54019}}
(see remark 8.8 of {{doi:10.1007/978-1-4615-7819-2}} for the definition of Hewitt realcompactification).
(see remark 8.8 of {{zb:1380.46022}} for the definition of Hewitt realcompactification).
4 changes: 2 additions & 2 deletions spaces/S000216/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
uid: S000216
name: Katětov's non-normal subspace of $\beta\mathbb{N}$
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

Fix a bijection $\varphi:\mathbb{N}\to\mathbb{Q}$. For each irrational $r$ fix a sequence of rational numbers $s_n\to r$, and let $E_r = \{\varphi^{-1}(s_n) : n\in\mathbb{N}\}$. Let $\mathcal{E} = \{E_r : r\in\mathbb{R}\setminus\mathbb{Q}\}$. Let $E'$ be the set of limit points for a subset $E$ of {S108}. Then $E'\neq \emptyset$ for $E \in\mathcal{E}$. For each $E\in\mathcal{E}$ pick some $p_E\in E'$.

Katětov's non-normal subspace of $\beta\mathbb{N}$ is the space $X=\mathbb{N}\cup D$ where $D = \{p_E : E\in\mathcal{E}\}$.

Constructed in exercise 6Q of {{doi:10.1007/978-1-4615-7819-2}}.
Constructed in exercise 6Q of {{zb:1380.46022}}.
2 changes: 1 addition & 1 deletion theorems/T000382.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ then:
refs:
- doi: 10.1090/S0002-9939-1973-0322812-9
name: Certain Subsets of Products of θ-refinable Spaces are Realcompact (P. Zenor)
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

Expand Down
4 changes: 2 additions & 2 deletions theorems/T000383.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,12 @@ if:
then:
P000164: true
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
- wikipedia: Measurable_cardinal
name: Measurable cardinal on Wikipedia
---

See Theorem 12.5 in {{doi:10.1007/978-1-4615-7819-2}}: in ZFC a measurable cardinal must be strongly inaccessible.
See Theorem 12.5 in {{zb:1380.46022}}: in ZFC a measurable cardinal must be strongly inaccessible.

Also {{wikipedia:Measurable_cardinal}}.
4 changes: 2 additions & 2 deletions theorems/T000384.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@ then:
refs:
- zb: "0684.54001"
name: General Topology (Engelking, 1989)
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman and Jerison)
---

See Theorem 3.8.2 of {{zb:0684.54001}} (where the {P18} property assumes {P5}).

Also Theorem 8.2 of {{doi:10.1007/978-1-4615-7819-2}} (where all spaces are assumed {P6}).
Also Theorem 8.2 of {{zb:1380.46022}} (where all spaces are assumed {P6}).
10 changes: 2 additions & 8 deletions theorems/T000386.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$ are projections, then $\pi_\alpha(X)\subseteq X_\alpha$ is {P22} and {P53}, and so {P16} [(Explore)](https://topology.pi-base.org/spaces?q=pseudocompact+%2B+metrizable+%2B+%7Ecompact). It follows that $X$ is a closed subspace of the {P16} space $\prod_\alpha \pi_\alpha(X)$, and so {P16}.
4 changes: 2 additions & 2 deletions theorems/T000742.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ if:
then:
P000215: true
refs:
- doi: 10.1007/978-1-4615-7819-2
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

Expand All @@ -17,5 +17,5 @@ Every {P53} space is {P7} and {P194}
[(Explore)](https://topology.pi-base.org/spaces?q=Metrizable%2B%7ESubmetacompact).
So every subspace of $Y$ satisfies the hypotheses of {T382},
and hence is {P162}.
By Corollary 8.18 of {{doi:10.1007/978-1-4615-7819-2}}
By Corollary 8.18 of {{zb:1380.46022}}
every subspace of $X$ is {P162}.
9 changes: 9 additions & 0 deletions theorems/T000914.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
---
uid: T000914
if:
P000221: true
then:
P000012: true
---

{P12} spaces are precisely the spaces admitting a uniformity.
13 changes: 13 additions & 0 deletions theorems/T000915.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
---
uid: T000915
if:
P000162: true
then:
P000221: true
refs:
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

See Corollary 15.14 of {{zb:1380.46022}} for complete uniformity on a {P162} space.
Alternatively, a {P162} space is a closed subspace of product of {S25} and {S25|P53}.
16 changes: 16 additions & 0 deletions theorems/T000916.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
uid: T000916
if:
and:
- P000001: true
- P000164: true
- P000221: true
then:
P000162: true
refs:
- zb: "1380.46022"
name: Rings of Continuous Functions (Gillman & Jerison)
---

A {P221} {P1} space is {P6} [(Explore)](https://topology.pi-base.org/spaces?q=dieudonne+complete+%2B+T_0+%2B+not+completely+regular).
Now apply Theorem 15.20 of {{zb:1380.46022}}.
19 changes: 19 additions & 0 deletions theorems/T000917.md
Comment thread
Moniker1998 marked this conversation as resolved.
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
---
uid: T000917
if:
and:
- P000134: true
- P000030: true
then:
P000221: true
refs:
- zb: "1358.54001"
name: General Topology (Kelley)
---

By taking the Kolmogorov quotient we can assume $X$ is {P3}.
Assume $X$ is not {P221}. Since $X$ is {P207} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+strongly+collectionwise+normal), the neighbourhoods of the diagonal $\Delta_X\subseteq X\times X$ form a uniformity $\mathcal{U}$ on $X$, and since $X$ is {P12} [(Explore)](https://topology.pi-base.org/spaces?q=R_1+%2B+paracompact+%2B+not+completely+regular), the uniformity is compatible with $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 cluster points (see Theorem 6.21 on page 191 of {{zb:1358.54001}}), 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 on page 156 of {{zb:1358.54001}}, the open cover $\{U_x : x\in X\}$ is even, so there exists $V\in\mathcal{U}$ such that each $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$.
Loading