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 triangle inequality
Statement
Let be an ordered field (Ordered field) and let . Then
Facts & Assumptions
Given: An ordered field and elements .
For every , , and equals or (Basic properties of the absolute value).
Order compatible with addition: if and , then . Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those (, and with giving ); the nonstrict form used here is those two together with the cases and , settled by trichotomy, the order being total (Ordered field). Explicitly: if and the second strict form applies; if and the first gives ; if and the first gives ; and if and the two sides are equal.
Field and order arithmetic: , and (Ordered field).
Proof
By [L1], and .
Adding the two chains of [step 1.1] with [L2] and using from [L3] gives .
By [L1] the value equals or ; both and hold by [step 2.1] and [L3] (the latter from ), so .
Depends on
Used by
- The reverse triangle inequality Corollary
- The total-variation bound for a Riemann–Stieltjes integral Corollary
- The uniform limit of uniformly continuous real-valued functions is uniformly continuous Corollary
- On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
- The hyperbola {(x,y) : xy = 1} is closed in ℝ² and its image under the first projection is ℝ ∖ {0}, which is not closed Counterexample
- Two copies of ℝ glued along ℝ ∖ {0} give a non-Hausdorff quotient of a metrizable space, by an open quotient map Counterexample
- ℤ is closed and not compact, and (0,1) is bounded and not compact: neither hypothesis of Heine-Borel can be dropped Counterexample
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms Definition
- Limits at +∞ and -∞, and infinite limits at a point Definition
- Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field Definition
- The oscillation ω_f(S) = sup{ |f(x) - f(y)| : x, y ∈ S } of f on a set and the oscillation ω_f(c) = inf_δ > 0 ω_f(A ∩ N_δ(c)) at a point, both taken in the extended reals Definition
- The topology of compact convergence on C(X,Y) for metric X and Y: uniform convergence on each compact subset of X Definition
- The ε-neighbourhood and the punctured ε-neighbourhood of a point of ℝ Definition
- The absolute-value function is convex Example
- The diagonal of ℝ is closed in ℝ², computed from the product basis Example
- The Hilbert cube [0,1]^ℕ with the product topology is metrizable, by d(x,y) = ∑ₖ |xₖ - yₖ| / 2^ k+1 Example
- The map (x,z) ↦ x · z on ℝ × ℝ and its transpose z ↦ (x ↦ x · z) traced through the exponential law Example
- The map x↦ x/(1+|x|) is a uniformly continuous homeomorphism from ℝ to (-1,1) whose inverse is not uniformly continuous Example
- Young's theorem integrates a Hölder function of unbounded variation against itself Example
- FALSE: a quotient of a Hausdorff space is Hausdorff False statement
- FALSE: all norms on a real vector space are equivalent False statement
- FALSE: the projections of a product are closed maps False statement
- A Cauchy sequence with a convergent subsequence converges, to that subsequence’s limit Lemma
- A compact subset of ℝ is closed and bounded Lemma
- A sequence has at most one limit Lemma
- At a limit point of the domain a function has at most one limit Lemma
- Each ‖·‖ₚ is a norm on ℝⁿ, and the induced metrics are exactly d₁, d₂ and d_∞ of the published metric-spaces page Lemma
- Every Cauchy sequence of reals is bounded Lemma
- Every convergent sequence is bounded Lemma
- Every convergent sequence is Cauchy Lemma
- Homogeneity and subadditivity of total variation Lemma
- If f has a finite limit at c then f is bounded on some punctured neighbourhood of c Lemma
- If for every ε > 0 some continuous g : X → ℝ satisfies | f(x) - g(x)| < ε for all x, then f is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum Lemma
- Products converge uniformly when both factors converge uniformly and one limiting factor and one approximating family are uniformly bounded Lemma
- Refinement and tag-change estimates for Stieltjes sums Lemma
- ℝⁿ as the set of functions n → ℝ, and d₁, d₂, d_∞ are metrics on it Lemma
- Samuel function pseudometrics generate a uniformity coarser than the original one Lemma
- Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges Lemma
- The absolute value makes ℝ 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 Lemma
- The monotone convergence property plus the Archimedean property imply the least-upper-bound property Lemma
…and 24 more results.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 8 results over 5 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
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed. (standard reference, not scraped)
- Purdue University analysis notes: Ordered fields and absolute value (standard reference, not scraped)