Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Assuming dependent choice, a nonempty topological space is separated-uniformizable if and only if it is Tychonoff
Statement
Assuming dependent choice, a nonempty topological space is separated-uniformizable if and only if it is Tychonoff.
Facts & Assumptions
Given: A nonempty topological space and dependent choice.
Uniformizable is equivalent to completely regular under dependent choice (Assuming dependent choice, a nonempty topological space is uniformizable if and only if it is completely regular).
A separated compatible uniformity induces a Hausdorff topology (A uniformity is separated if and only if its induced topology is Hausdorff).
Tychonoff means completely regular plus (Completely regular spaces and Tychonoff () spaces, (Kolmogorov) and (Frechet) spaces).
A completely regular topology is induced by the gauge over all continuous (The topology of a nonempty completely regular space is induced by the gauge of its continuous -valued pseudometrics, A gauge of pseudometrics and, on a nonempty set, the uniformity it generates).
Every Hausdorff space is (Every Urysohn space is Hausdorff, every Hausdorff space is and hence , and every regular space is Urysohn, clause 2).
In a space every singleton is closed (A space is if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology, clause (b)).
Proof
A separated-uniformizable space is completely regular by [L1] and Hausdorff by [L2], hence by [L5] and therefore Tychonoff by [L3].
Conversely, let be Tychonoff. For , the singleton is closed by [L6], and complete regularity gives a continuous with and . Thus the gauge in [L4] has an entourage excluding , so its intersection is the diagonal and it is separated. It induces the original topology by [L4].
Thus it is separated-uniformizable, proving the converse and the equivalence.
Depends on
- Assuming dependent choice, a nonempty topological space is uniformizable if and only if it is completely regular
- A uniformity is separated if and only if its induced topology is Hausdorff
- Completely regular spaces and Tychonoff ($T_{3\frac{1}{2}}$) spaces
- $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- The topology of a nonempty completely regular space is induced by the gauge of its continuous $[0,1]$-valued pseudometrics
- A gauge of pseudometrics and, on a nonempty set, the uniformity it generates
- Every Urysohn space is Hausdorff, every Hausdorff space is $T_1$ and hence $T_0$, and every regular $T_1$ space is Urysohn
- A space is $T_1$ if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology
Used by
- Under dependent choice and the ultrafilter lemma, the Stone-Cech compactification maps continuously onto the Samuel compactification Corollary
- Under dependent choice and the ultrafilter lemma, the Samuel compactification of the discrete natural numbers is beta N Example
- Under the ultrafilter lemma the Samuel completion is compact, and under dependent choice plus the ultrafilter lemma it compactifies every separated uniform space Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 105 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Wodzicki, Uniform Structure (standard reference, not scraped)
- M. Kunzinger, General Topology (standard reference, not scraped)
- M. Megrelishvili, Lecture Notes in Topological Groups (standard reference, not scraped)