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.
Every uniformizable space is regular
Statement
Every uniformizable topological space is regular, in ZF.
Facts & Assumptions
Given: A topology induced by a uniformity, a closed , and .
Entourage balls form neighbourhood bases and entourages have iterated square roots (The sets containing an entourage ball about each of their points form a topology, Uniform space in the entourage formulation).
Regularity separates a point from a closed set by disjoint open sets (Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly).
Symmetric entourages have square roots, and a point is outside the closure of a set when it has a neighbourhood disjoint from that set (Every uniformity has a base of symmetric entourages, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
Proof
Since is an open neighbourhood of , choose an entourage with , then choose a symmetric with .
Let be the union of all open subsets of containing . Then is open and because is a neighbourhood.
One has . Indeed, if , then the neighbourhood is disjoint from : a point would give by symmetry. Hence by [L3].
Since , step 2.1 gives . The two open sets and are disjoint neighbourhoods of and , so the space is regular by [L2].
Depends on
- Uniformizable and separated-uniformizable topological spaces
- Uniform space in the entourage formulation
- The sets containing an entourage ball about each of their points form a topology
- Regular spaces and $T_3$ spaces, with the source disagreement over whether regularity includes $T_1$ stated explicitly
- Every uniformity has a base of symmetric entourages
- Interior, closure, boundary, exterior, derived set and isolated point in a topological space
Used by
- The K-topology on ℝ is not uniformizable Counterexample
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 36 results over 14 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)