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.
A uniformity is separated if and only if its induced topology is Hausdorff
Statement
The topology induced by a uniformity is Hausdorff if and only if is separated.
Facts & Assumptions
Given: A uniform space with its induced topology.
A uniformity is separated exactly when each distinct pair is excluded by an entourage (Separated uniformity: the intersection of all entourages is the diagonal).
Entourage balls are neighbourhood bases, and symmetric square roots exist (The sets containing an entourage ball about each of their points form a topology, Every uniformity has a base of symmetric entourages).
Hausdorff means that distinct points have disjoint open neighbourhoods (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
Proof
Suppose is separated and . Choose with , then a symmetric with .
Conversely, if the induced topology is Hausdorff and , choose disjoint neighbourhoods of and refine the first by an entourage ball ; then , so .
The neighbourhoods and are disjoint: if belonged to both, symmetry would give and hence .
Thus the induced topology is Hausdorff by [L2].
Every distinct pair is excluded by an entourage, so is separated by [A1].
Depends on
- Separated uniformity: the intersection of all entourages is the diagonal
- The sets containing an entourage ball about each of their points form a topology
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Every uniformity has a base of symmetric entourages
Used by
- Assuming dependent choice, a nonempty topological space is separated-uniformizable if and only if it is Tychonoff Corollary
- The Samuel reflection of a nonempty indiscrete uniform space is a singleton Example
- Under dependent choice and the ultrafilter lemma, the Samuel compactification of a nonempty compact Hausdorff space adds no points up to unique uniform isomorphism Example
- Every uniform space has a Hausdorff completion with dense canonical image, and the canonical map is a uniform embedding exactly when the original uniformity is separated Theorem
- Under dependent choice and the ultrafilter lemma, uniformly continuous maps to compact Hausdorff spaces extend uniquely over the Samuel compactification Theorem
- 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 · two levels
13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. Wodzicki, Uniform Structure (standard reference, not scraped)
- Encyclopedia of Mathematics, Uniform space (standard reference, not scraped)