Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (claude-sonnet-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.

For a nonempty set X and a metric space (Y,d) the uniform metric ρˉ(f,g)=supxmin{d(f(x),g(x)),1} is a metric on YX

Statement

Let X be a nonempty set, let (Y,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and write

dˉ(u,v)  :=  min{d(u,v), 1}(u,vY),

which is a metric on Y with dˉ1 everywhere (min(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology, claims 1 and 2). For f,gYX (The topology of pointwise convergence on YX, which is the product topology, and its restriction to C(X,Y)) put

R(f,g)  :=  {dˉ(f(x),g(x)):xX}R,ρˉ(f,g)  :=  supR(f,g).

This is well defined: R(f,g) is nonempty because X is, and 1 is an upper bound of it, so the least upper bound exists (Complete ordered field (least-upper-bound property)) and is unique (Suprema and infima are unique).

Then ρˉ is a metric on YX (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric), the uniform metric, and ρˉ(f,g)1 for all f,g.

Both hypotheses are used and neither is decoration. Nonemptiness of X is what makes R(f,g) nonempty; for X= the set YX has a single element, but sup is undefined under the real-valued supremum convention used here (Conventions: sup, unbounded sets, and the extended reals). The extended real line is introduced later and is not the codomain of this metric. Truncating d at 1 is what makes R(f,g) bounded above with no boundedness hypothesis on f and g; that is the whole reason the truncation is there.

Facts & Assumptions

Given: A nonempty set X, a metric space (Y,d), functions f,g,hYX, a fixed x0X, and dˉ, R, ρˉ as displayed above.

[L2]

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

[L3]

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, with the case of equality settled by totality of the order, in the nonstrict form; and a0 together with a0 gives a=0 (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

For all f,gYX the set R(f,g) is nonempty, since x0X contributes dˉ(f(x0),g(x0)), and 1 is an upper bound of it by [L1]; so ρˉ(f,g)=supR(f,g) exists, is unique, and satisfies ρˉ(f,g)1.

givenL1L2
2.1

ρˉ(f,g)dˉ(f(x),g(x))0 for every xX, a supremum being an upper bound of its set and dˉ being nonnegative.

step 1.1L1L2
2.2

Symmetry (M2): dˉ(g(x),f(x))=dˉ(f(x),g(x)) for every x by (M2) for dˉ, so R(g,f) and R(f,g) are the same subset of R and have the same supremum.

step 1.1L1L2
2.3

Separation (M1), the other direction: if f=g then R(f,g)={0} by (M1) for dˉ, and the least upper bound of {0} is 0, so ρˉ(f,g)=0.

step 1.1L1L2
3.1

Separation (M1), one direction: if ρˉ(f,g)=0 then for every xX we have dˉ(f(x),g(x))0 by step 2.1 and dˉ(f(x),g(x))0 by [L1], hence dˉ(f(x),g(x))=0, hence f(x)=g(x) by (M1) for dˉ; so f=g, two elements of YX being equal exactly when they agree at every point.

step 2.1L1L3
3.2

For every xX: dˉ(f(x),h(x))dˉ(f(x),g(x))+dˉ(g(x),h(x))ρˉ(f,g)+ρˉ(g,h), by (M3) for dˉ and because each supremum bounds its own set above.

step 1.1step 2.1L1L2L3
4.1

Triangle inequality (M3): by step 3.2 the real number ρˉ(f,g)+ρˉ(g,h) is an upper bound of R(f,h), and ρˉ(f,h) is the least upper bound of that set, so ρˉ(f,h)ρˉ(f,g)+ρˉ(g,h).

step 3.2L2
5.1

The function ρˉ:YX×YXR therefore satisfies (M1) by steps 3.1 and 2.3, (M2) by step 2.2 and (M3) by step 4.1, so it is a metric on YX, and ρˉ1 by step 1.1.

step 1.1step 2.2step 3.1step 2.3step 4.1L1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 18 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