Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)
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 supremum metric d∞(f,g)=sup⁡x∣f(x)−g(x)∣ is a metric on the bounded real-valued functions on a nonempty set

Statement

Let S be a nonempty set. Call a function f:S→R bounded when its range f[S]={f(s):s∈S} is a bounded subset of R (Lower bound, bounded below, bounded set), and write

B(S):={ f:f is a bounded function S→R }.

For f,g∈B(S) put D(f,g):={ ∣f(s)−g(s)∣:s∈S } and

d∞(f,g):=sup⁡D(f,g).

This is well defined: D(f,g) is nonempty because S is, and it is bounded above (step 1.1 below), so its least upper bound exists (Complete ordered field (least-upper-bound property)) and is unique (Suprema and infima are unique).

Then d∞ is a metric on B(S) (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric), the supremum metric (also called the uniform metric).

The hypotheses ensure that the formula is a finite real-valued metric for every pair in the stated function space. Boundedness of f and g makes D(f,g) bounded above, and nonemptiness of S makes it nonempty. Some unbounded pairs can still have a finite supremum, but allowing all real-valued functions would not give a finite-valued metric: for example, on S=R the functions f(s)=s and g(s)=0 make D(f,g) unbounded above (Conventions: sup⁡∅, unbounded sets, and the extended reals).

Facts & Assumptions

Given: A nonempty set S and bounded functions f,g,h∈B(S), with ℓf≤f(s)≤uf, ℓg≤g(s)≤ug and ℓh≤h(s)≤uh for all s∈S; a fixed s0∈S.

[L1]

Bounded subset of R: T is bounded when there are ℓ,u∈R with ℓ≤t≤u for every t∈T (Lower bound, bounded below, bounded set).

[L2]

Least-upper-bound property: a nonempty subset of R that is bounded above has a least upper bound, that is an upper bound below every upper bound; it is unique (Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L3]

Absolute value: ∣u∣≥0; ∣u∣=0 if and only if u=0; ∣−u∣=∣u∣; and ∣u∣ equals u or −u (Basic properties of the absolute value, Absolute value in an ordered field).

[L4]

Two-term triangle inequality: ∣u+v∣≤∣u∣+∣v∣ (The triangle inequality).

[L5]

A two-element subset of R has a maximum, which is one of the two elements and bounds both (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L6]

Order arithmetic: inequalities may be added and a constant added to both sides, in the strict form of Order is preserved by adding a constant and by adding inequalities and, together with the case of equality settled by totality (Ordered field, Complete ordered field (least-upper-bound property)), in the nonstrict form used below; and by trichotomy a≤0 together with a≥0 gives a=0.

Proof

technique · direct
1.1

For every s∈S the value ∣f(s)−g(s)∣ is f(s)−g(s) or g(s)−f(s), and f(s)−g(s)≤uf−ℓg while g(s)−f(s)≤ug−ℓf; so M:=max⁡{uf−ℓg, ug−ℓf} bounds D(f,g) above, and since s0∈S makes D(f,g) nonempty, d∞(f,g)=sup⁡D(f,g) exists and is unique.

givenL1L2L3L5L6
1.2

Symmetry (M2): ∣g(s)−f(s)∣=∣−(f(s)−g(s))∣=∣f(s)−g(s)∣ for every s∈S, so D(g,f) and D(f,g) are the same subset of R and therefore have the same supremum.

L2L3
2.1

Separation (M1): d∞(f,g) bounds D(f,g) above, so d∞(f,g)≥∣f(s0)−g(s0)∣≥0; if d∞(f,g)=0 then ∣f(s)−g(s)∣≤0 and ∣f(s)−g(s)∣≥0 for every s, hence f(s)=g(s) for every s and f=g; conversely if f=g then D(f,g)={0}, whose least upper bound is 0.

step 1.1L2L3L6
2.2

For every s∈S: ∣f(s)−h(s)∣=∣(f(s)−g(s))+(g(s)−h(s))∣≤∣f(s)−g(s)∣+∣g(s)−h(s)∣≤d∞(f,g)+d∞(g,h), the last inequality because each supremum bounds its own set above.

step 1.1L2L4L6
3.1

Triangle inequality (M3): step 2.2 says the real number d∞(f,g)+d∞(g,h) is an upper bound of D(f,h), and d∞(f,h) is the least upper bound of that set, so d∞(f,h)≤d∞(f,g)+d∞(g,h).

step 2.2L2
4.1

The function d∞ therefore satisfies (M1) by step 2.1, (M2) by step 1.2 and (M3) by step 3.1, so it is a metric on B(S).

step 1.2step 2.1step 3.1∎

Remarks

Depends on

Used by

Dependency tree · two levels

29 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