Alphabeta MathHow 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
Statement
Let be an ordered field (Ordered field) and let . Then
Facts & Assumptions
Given: An ordered field and elements .
Triangle inequality: for all (The triangle inequality).
For every , , and equals or (Basic properties of the absolute value).
Proof
Applying [L1] with and gives , so .
Applying [L1] with and , and using from [L2], gives , so .
By [L2] the value equals or , and each of these is by steps 1.1 and 1.2, so .
Depends on
Used by
- |x| is Lipschitz and absolutely continuous but not C¹ on [-1,1] Example
- x · 1_ℚ(x) is continuous at 0 and at no other point Example
- If lim_x → c f(x) = L ≠ 0 then |f| > |L|/2 on a punctured neighbourhood of c; in particular if L > 0 then f > L/2 > 0 there Lemma
- The absolute value is compatible with limits Lemma
- Algebra of limits: sums, scalar multiples, products and quotients Theorem
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in ℝᵐ Theorem
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function Theorem
Dependency tree · two levels
8 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
- 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)