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.
on has the usual topology and diameter at most
Example
On , let be the usual metric (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded) and put
Then:
- is a metric on , uniformly equivalent and therefore topologically equivalent to (Topologically, uniformly and Lipschitz equivalent metrics on a set, Lipschitz equivalence implies uniform equivalence implies topological equivalence); so has exactly the usual topology of the real line.
- is a bounded metric space and in the metric (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), whereas is not bounded at all and has no diameter.
This is the concrete instance of and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology on the real line, and it is the witness used for the failure of two plausible-sounding claims: that boundedness is topological, and that topologically equivalent metrics are Lipschitz equivalent.
Facts & Assumptions
Given: The real line with and the function ; the set .
is a metric on and is not bounded, so it has no diameter (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded, Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).
For any metric , the function is a metric, is bounded with diameter at most on a nonempty space, and is uniformly equivalent to ( and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology).
Uniform equivalence implies topological equivalence (Lipschitz equivalence implies uniform equivalence implies topological equivalence, Topologically, uniformly and Lipschitz equivalent metrics on a set).
The minimum of a two-element set of reals exists and is one of them (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); and (Basic properties of the absolute value, Absolute value in an ordered field, The multiplicative identity is positive).
The diameter is the least upper bound of the set of distances, so it is every distance and every upper bound of them; and it is unique (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Suprema and infima are unique, Complete ordered field (least-upper-bound property), Ordered field).
Verification
By [L1] the function is a metric on and is not bounded in it.
, so .
By [L2] applied to : is a metric on , the space is bounded, in , and is uniformly equivalent to .
Claim 2: the diameter of in is an upper bound of and by step 1.2, so it is ; combined with from step 2.1 this gives in the metric , while by step 1.1 the space has no diameter at all in .
Claim 1: is a metric uniformly equivalent to by step 2.1, hence topologically equivalent to it, so the metric topology of is the usual topology of .
Claims 1 and 2 hold by steps 3.2 and 3.1.
Remarks
- Nothing about is special here except unboundedness. The same computation on any unbounded metric space gives a bounded metric with the same topology ( and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology); the real line is chosen because it is the space every reader already has.
- The diameter is exactly and not less, which is what step 1.2 contributes: for the construction the bound of and are metrics uniformly equivalent to , so every metric space carries a bounded metric with the same topology is attained as soon as takes some value , because the new metric then takes the value itself.
- The two metrics are not Lipschitz equivalent, so this pair also witnesses the strictness of the first implication of Lipschitz equivalence implies uniform equivalence implies topological equivalence; that computation is On the metrics and are uniformly but not Lipschitz equivalent.
Depends on
- $\min(d,1)$ and $d/(1+d)$ are metrics uniformly equivalent to $d$, so every metric space carries a bounded metric with the same topology
- Topologically, uniformly and Lipschitz equivalent metrics on a set
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- Maximum and minimum of a set
- 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
- Lipschitz equivalence implies uniform equivalence implies topological equivalence
- Every nonempty finite set of reals has a maximum and a minimum
- Basic properties of the absolute value
- Absolute value in an ordered field
- The multiplicative identity is positive
- Suprema and infima are unique
- Complete ordered field (least-upper-bound property)
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- Ordered field
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 65 results over 19 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
- Equivalence of metrics (Wikipedia) (standard reference, not scraped)
- Metric space (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §20 (standard reference, not scraped)
- R. Gardner, Introduction to Topology, notes on Munkres Section 20: The Metric Topology (East Tennessee State University) (standard reference, not scraped)