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.
The reverse triangle inequality in any metric space
Statement
Let be a metric space (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric) and let . Then
where is the absolute value of (Absolute value in an ordered field).
Facts & Assumptions
Given: A metric space and points ; write .
The triangle inequality (M3): for all (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
Symmetry (M2): for all (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
For every real , the value equals or (Basic properties of the absolute value, Absolute value in an ordered field).
Adding a constant to an inequality: if then . Order is preserved by adding a constant and by adding inequalities states the strict form ; the nonstrict form used here is that strict form together with the case , in which the two sides are equal, the order being total (Ordered field, Complete ordered field (least-upper-bound property)).
Proof
By [A1] at : .
By [A1] at : , and by [A2] , so .
Adding to both sides of step 1.1 gives .
Adding to both sides of step 1.2 gives , that is .
By [L1] the real number is either or , and both of these are at most by steps 2.1 and 2.2, so .
Remarks
- Read with fixed, this says the function does not increase distances: its values at and at differ by at most . That is the model for , so the distance to a fixed nonempty set is -Lipschitz, which proves the same estimate with the point replaced by a nonempty set.
- The inequality specialises, on with (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded), to the familiar .
Depends on
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- Basic properties of the absolute value
- Order is preserved by adding a constant and by adding inequalities
- Ordered field
- Absolute value in an ordered field
- Complete ordered field (least-upper-bound property)
Used by
- 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
- The topology of compact convergence on C(X,Y) for metric X and Y: uniform convergence on each compact subset of X Definition
- A Lipschitz function on ℚ extends uniquely to a Lipschitz function on ℝ with the same constant Example
- The bounded real-valued functions on a set, with the supremum metric, form a complete metric space Example
- |d(x,A) - d(y,A)| ≤ d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz Lemma
- A completion is unique up to a unique isometry fixing the original space, and uniformly continuous maps into complete spaces extend through it Theorem
- Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed Theorem
- Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 19 results over 6 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
- Triangle inequality (Wikipedia) (standard reference, not scraped)
- Metric space (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)