Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric

Definition

Throughout, R\mathbb{R} is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) constructed in this library (The real numbers) and carrying its order (Order on the reals).

Let XX be a set. A metric on XX is a function d:X×XRd : X \times X \to \mathbb{R} such that for all x,y,zXx, y, z \in X:

  • (M1) Separation. d(x,y)=0d(x,y) = 0 if and only if x=yx = y.
  • (M2) Symmetry. d(x,y)=d(y,x)d(x,y) = d(y,x).
  • (M3) Triangle inequality. d(x,z)d(x,y)+d(y,z)d(x,z) \le d(x,y) + d(y,z).

A metric space is a pair (X,d)(X,d) consisting of a set XX and a metric dd on it. The elements of XX are its points and d(x,y)d(x,y) is the distance from xx to yy. When only one metric is in play we write XX for (X,d)(X,d); when several are, the metric is always named.

The values of a metric are real numbers. The codomain is R\mathbb{R}, so d(x,y)d(x,y) is an honest element of the complete ordered field and every inequality above is an inequality there. No infinite value is permitted; Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here records why extended metrics are not treated in this library.

Nonnegativity is deliberately absent from the axiom list. Many texts add a fourth axiom d(x,y)0d(x,y) \ge 0. It is redundant: (M1), (M2) and (M3) already force it, as Nonnegativity of a metric is a consequence of the other axioms, not an axiom proves. Nothing below assumes it before that lemma is available.

Pseudometric. A pseudometric on XX is a function p:X×XRp : X \times X \to \mathbb{R} satisfying (M2), (M3) and the weakening

  • (M1') Reflexivity. p(x,x)=0p(x,x) = 0 for every xXx \in X

of (M1). A pseudometric may therefore assign distance 00 to two distinct points. Every metric is a pseudometric, and a pseudometric is a metric exactly when p(x,y)=0p(x,y) = 0 forces x=yx = y.

Ultrametric. An ultrametric on XX is a metric dd that in addition satisfies

  • (M3') Strong triangle inequality. d(x,z)max{d(x,y),d(y,z)}d(x,z) \le \max\{d(x,y), d(y,z)\}

for all x,y,zXx, y, z \in X, where the maximum is that of a two-element subset of R\mathbb{R}, which exists and is one of the two elements (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum). An ultrametric space is a pair (X,d)(X,d) with dd an ultrametric.

Remarks

Depends on

Used by

…and 129 more results.

Dependency tree · next 3 levels

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