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.
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) constructed in this library (The real numbers) and carrying its order (Order on the reals).
Let be a set. A metric on is a function such that for all :
- (M1) Separation. if and only if .
- (M2) Symmetry. .
- (M3) Triangle inequality. .
A metric space is a pair consisting of a set and a metric on it. The elements of are its points and is the distance from to . When only one metric is in play we write for ; when several are, the metric is always named.
The values of a metric are real numbers. The codomain is , so is an honest element of the complete ordered field and every inequality above is an inequality there. No infinite value is permitted; Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here records why extended metrics are not treated in this library.
Nonnegativity is deliberately absent from the axiom list. Many texts add a fourth axiom . It is redundant: (M1), (M2) and (M3) already force it, as Nonnegativity of a metric is a consequence of the other axioms, not an axiom proves. Nothing below assumes it before that lemma is available.
Pseudometric. A pseudometric on is a function satisfying (M2), (M3) and the weakening
- (M1') Reflexivity. for every
of (M1). A pseudometric may therefore assign distance to two distinct points. Every metric is a pseudometric, and a pseudometric is a metric exactly when forces .
Ultrametric. An ultrametric on is a metric that in addition satisfies
- (M3') Strong triangle inequality.
for all , where the maximum is that of a two-element subset of , which exists and is one of the two elements (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum). An ultrametric space is a pair with an ultrametric.
Remarks
-
(M3') is a genuine strengthening of (M3), not an independent axiom on top of it. A function satisfying (M1), (M2) and (M3') automatically satisfies (M3): by Nonnegativity of a metric is a consequence of the other axioms, not an axiom such a function is nonnegative, and for nonnegative reals one has , since the maximum is one of and the other summand is . So "a metric satisfying (M3')" and "a function satisfying (M1), (M2), (M3')" describe the same objects, and the definition above may be read either way.
-
Why the biconditional form of (M1). Splitting (M1) into "" and "" gives the same notion; the split form is what makes the pseudometric weakening above a matter of deleting one clause. The naming fork between pseudometric and semimetric, which is live in the literature, is settled for this library in Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here.
-
The metric is part of the data. Two different metrics on the same set are two different metric spaces, even when they have the same open sets. That is why Topologically, uniformly and Lipschitz equivalent metrics on a set compares metrics at three separate strengths rather than one, and why a property can be invariant under one of them and not under another (FALSE: boundedness of a metric space is determined by its topology).
Depends on
Used by
- A uniformly continuous real function on a subset D ⊆ ℝ extends uniquely to a uniformly continuous function on the closure of D Corollary
- The a priori bound d(x^*, xₙ) ≤ qⁿ d(x₁,x₀)/(1-q) and the a posteriori bound d(x^*, xₙ₊₁) ≤ q d(xₙ₊₁,xₙ)/(1-q) Corollary
- Under choice and dependent choice, metric open covers admit locally finite subordinate partitions of unity Corollary
- Boundedness does not replace pointwise relative compactness for an arbitrary metric target Counterexample
- g(x,y) = xy/(x²+y²), extended by g(0,0)=0, is continuous in each variable separately and not continuous at the origin Counterexample
- In {0} ∪ [1,2] with the metric of ℝ, the closure of B(0,1) = {0} is {0} while the closed ball is {0,1} Counterexample
- In the bounded real-valued functions on ℕ with the supremum metric, the closed unit ball is closed and bounded and is not compact: the indicator functions of the singletons are pairwise at distance 1 Counterexample
- In the discrete metric the boundary of B(p,1) is empty while the sphere of radius 1 is everything but p Counterexample
- ℕ with the discrete metric is bounded and is not totally bounded Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| have the same topology and are not uniformly equivalent Counterexample
- On (0,∞) the metrics |x-y| and |1/x - 1/y| share their topology and not their Cauchy sequences Counterexample
- On (0,1) the identity is bounded with no greatest value and x ↦ 1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain Counterexample
- On ℕ with d(m,n) = 1 + 1/(m+n) for m ≠ n the sets {n, n+1, …} are nested, closed, bounded and complete with empty intersection Counterexample
- On ℝ the metrics |x-y| and min(|x-y|,1) are uniformly but not Lipschitz equivalent Counterexample
- On the positive integers the metrics |m-n| and |1/m - 1/n| both induce the discrete topology, and only the first is complete Counterexample
- ℝ carries both an unbounded and a bounded metric inducing the same topology Counterexample
- Refuted: a pointwise bounded family of continuous functions is equicontinuous. The spikes are bounded by 1 everywhere and are not equicontinuous at 0 Counterexample
- Refuted: C(X,Y) is closed in the topology of pointwise convergence. The ramps on [0,1] converge pointwise to a discontinuous limit Counterexample
- The cover of (0,1) by the intervals (1/(k+2), 1) has no Lebesgue number, so the Lebesgue number lemma needs compactness Counterexample
- The indiscrete topology on a two-point set is induced by no metric Counterexample
- The open interval (0,1) is totally bounded and not compact, the cover by the intervals (1/(k+2), 1) having no finite subcover Counterexample
- The Samuel compactification map need not be a uniform embedding for the original uniformity Counterexample
- Two copies of ℝ glued along ℝ ∖ {0} give a non-Hausdorff quotient of a metrizable space, by an open quotient map Counterexample
- x ↦ √x is a uniformly continuous bijection of [0,∞) onto itself whose inverse x ↦ x² is not uniformly continuous Counterexample
- x ↦ 1/x is continuous on (0,1) and not uniformly continuous, so Heine-Cantor needs compactness of the domain Counterexample
- x ↦ 1/x is continuous on (0,1) and sends the Cauchy sequence (1/(k+2))_k ≥ 0 to an unbounded one Counterexample
- x ↦ x + 1/x on [1,∞) strictly decreases every distance and has no fixed point Counterexample
- x ↦ x/2 maps (0,1] into itself, is a 1/2-contraction, and has no fixed point Counterexample
- ℤ and {n + 1/n : n ≥ 2} are disjoint closed subsets of ℝ at distance 0, so the set-to-set distance is not a metric Counterexample
- A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace Definition
- A gauge of pseudometrics and, on a nonempty set, the uniformity it generates Definition
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms Definition
- Bilipschitz embeddings and bilipschitz equivalences of metric spaces Definition
- Bounded distance between two maps into a metric space Definition
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space Definition
- Bounded-edge coarse fillings of loops and triangles Definition
- Cauchy sequence in a metric space Definition
- Coarse Lipschitz maps and quasi-isometric embeddings Definition
- Coarsely dense subsets, quasi-inverses and quasi-isometries Definition
- Complete metric space: every Cauchy sequence converges in the space Definition
…and 179 more results.
Dependency tree · two levels
12 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
- Metric space (Wikipedia) (standard reference, not scraped)
- Ultrametric space (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)
- T. Tao, Analysis II, 3rd ed., Ch. 1 (standard reference, not scraped)
- Pseudometric space (Wikipedia) (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)