ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-09-05

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.

A Lawvere metric space as an enriched category

Example

Let $(X, d)$ be a metric space. Regard $[0, \infty]$ as a preorder with the reverse order $\geq$ , tensor product $+$ , and unit $0$ . Defining the hom-object from $x$ to $y$ to be the number $d (x, y)$ makes $X$ into an $[0, \infty]$ -enriched category.

Facts & Assumptions

Given: A metric space $(X, d)$ .

[L1]

A metric satisfies $d (x, x) = 0$ and the triangle inequality (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

A $V$ -category is encoded by identities and composition in the base preorder (Enriched category over a monoidal base).

Verification

technique · direct

1.1

Because the unit of the base is $0$ , the identity axiom for [L2] is exactly the statement $0 \geq d (x, x)$ , which holds by [L1].

L1L2given

1.2

The composition axiom in the reversed-order preorder is $d (y, z) + d (x, y) \geq d (x, z)$ , which is exactly the triangle inequality from [L1].

L1L2

2.1

Therefore every metric space is a Lawvere-style enriched category over the base $([0, \infty], \geq, +, 0)$ .

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Emily Riehl, Categorical Homotopy Theory, Section 3.2 (standard reference, not scraped)