How 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.
The sets containing an entourage ball about each of their points form a topology
Statement
For a uniformity on , call open when every has an entourage with . These open sets form a topology on . Its neighbourhood filter at has as a base.
Facts & Assumptions
Given: A uniform space .
Entourages contain the diagonal, are closed under finite intersection, and have symmetric square roots (Uniform space in the entourage formulation, Every uniformity has a base of symmetric entourages).
A topology contains , is closed under arbitrary unions, and under binary intersections (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).
A neighbourhood base at refines every neighbourhood of (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).
Proof
The sets and are open: the first has no points to test, and for every entourage ball is contained in .
An arbitrary union of open sets is open, because a point in the union lies in one member and retains that member's entourage ball.
If , choose entourage balls and ; then , so binary intersections are open.
By steps 1.1 to 1.3, the open sets form a topology by [L1].
Let be an entourage and define This set is open. Indeed, given , choose as displayed and then a symmetric with . If , symmetry gives , so ; hence . Now choose a symmetric with . If , then , so . Thus , proving that is a neighbourhood of .
Conversely, if is a neighbourhood of , it contains an open set with ; the definition of the topology supplies an entourage with . Thus the entourage balls refine every neighbourhood, and by step 3.1 they are themselves neighbourhoods. They form a neighbourhood base by [L2].
Depends on
- Uniform space in the entourage formulation
- Every uniformity has a base of symmetric entourages
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open
Used by
- Every continuous map from a nonempty compact Hausdorff space to a uniform space is uniformly continuous Corollary
- Uniformizable and separated-uniformizable topological spaces Definition
- A Cauchy filter with a cluster point converges to that point Lemma
- A metric on a nonempty set generates an entourage uniformity whose induced topology and uniformly continuous maps are the usual metric notions, and this uniformity is separated Lemma
- Assuming dependent choice, every uniformizable space is completely regular Lemma
- Assuming dependent choice, the Samuel uniformity induces the original topology Lemma
- Every compact uniform space is totally bounded Lemma
- Every convergent filter on a uniform space is Cauchy Lemma
- Every uniformizable space is regular Lemma
- The minimal Cauchy filters associated to points define a uniformly continuous dense canonical map Lemma
- Total boundedness passes to a uniform space with a dense uniformly continuous image Lemma
- A nonempty compact Hausdorff space carries exactly one compatible uniformity Theorem
- A uniformity is separated if and only if its induced topology is Hausdorff Theorem
- Every uniformly continuous map is continuous for the induced topologies Theorem
- The covers admitting an open refinement form a compatible uniform-cover structure on a nonempty compact Hausdorff space; in particular every open cover is uniform Theorem
- The left and right uniformities of a topological group induce its topology, and inversion interchanges them Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 17 results over 11 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)