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
- 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
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space Definition
- Cauchy sequence in a metric space Definition
- Complete metric space: every Cauchy sequence converges in the space Definition
- Continuity of a map between metric spaces, at a point and globally, in the ε-δ form Definition
- Convergence of a sequence in a metric space: xₖ → x iff d(xₖ, x) → 0 in ℝ Definition
- Countably compact, sequentially compact and limit point compact metric spaces Definition
- Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces Definition
- Finite ε-net and totally bounded metric space Definition
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space Definition
…and 129 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 27 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
- 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)