Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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 ∣d(x,z)−d(y,z)∣≤d(x,y) in any metric space

Statement

Let (X,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let x,y,z∈X. Then

∣d(x,z)−d(y,z)∣≤d(x,y),

where ∣⋅∣ is the absolute value of R (Absolute value in an ordered field).

Facts & Assumptions

Given: A metric space (X,d) and points x,y,z∈X; write t:=d(x,z)−d(y,z).

[A1]

The triangle inequality (M3): d(a,c)≤d(a,b)+d(b,c) for all a,b,c∈X (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L1]

For every real u, the value ∣u∣ equals u or −u (Basic properties of the absolute value, Absolute value in an ordered field).

[L2]

Adding a constant to an inequality: if a≤b then a+c≤b+c. Order is preserved by adding a constant and by adding inequalities states the strict form a<b⇒a+c<b+c; the nonstrict form used here is that strict form together with the case a=b, in which the two sides are equal, the order being total (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

By [A1] at (a,b,c)=(x,y,z): d(x,z)≤d(x,y)+d(y,z).

A1
1.2

By [A1] at (a,b,c)=(y,x,z): d(y,z)≤d(y,x)+d(x,z), and by [A2] d(y,x)=d(x,y), so d(y,z)≤d(x,y)+d(x,z).

A1A2
2.1

Adding −d(y,z) to both sides of step 1.1 gives t=d(x,z)−d(y,z)≤d(x,y).

step 1.1L2
2.2

Adding −d(x,z) to both sides of step 1.2 gives d(y,z)−d(x,z)≤d(x,y), that is −t≤d(x,y).

step 1.2L2
3.1

By [L1] the real number ∣t∣ is either t or −t, and both of these are at most d(x,y) by steps 2.1 and 2.2, so ∣d(x,z)−d(y,z)∣=∣t∣≤d(x,y).

step 2.1step 2.2L1∎

Remarks

Depends on

Used by

Dependency tree · two levels

13 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