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.
The closed unit interval has exactly one compatible uniformity, namely its usual metric uniformity
Example
The interval , with its usual topology, has exactly one compatible uniformity, the restriction of the usual metric uniformity of .
Facts & Assumptions
Given: The usual topology and metric on .
The usual metric makes a metric space with its usual topology (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded).
A closed bounded subset of is compact (A subset of is compact if and only if it is closed and bounded).
A compact Hausdorff space has a unique compatible uniformity (A nonempty compact Hausdorff space carries exactly one compatible uniformity).
Verification
The interval is closed and bounded, hence compact by [L2], and its metric topology is Hausdorff by [L1].
Its restricted metric uniformity is compatible by the metric dictionary (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).
Uniqueness follows from [L3], so no other compatible uniformity exists.
Depends on
- A nonempty compact Hausdorff space carries exactly one compatible uniformity
- 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
- A subset of $\mathbb{R}$ is compact if and only if it is closed and bounded
- The absolute value makes $\mathbb{R}$ a metric space: $d(x,y) = |x-y|$ is a metric, its open balls are the intervals $(x-r, x+r)$, and it is unbounded
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 72 results over 15 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)