ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02

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.

Under dependent choice and the ultrafilter lemma, the Samuel compactification of the open unit interval is the closed unit interval

Example

Give $(0, 1)$ and $[0, 1]$ the subspace metric $d (s, t) = ∣ s - t ∣$ from the usual real metric (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Isometry, isometric embedding, and the subspace metric on a subset) and the uniformities that it generates. With these metric uniformities, the inclusion $i : (0, 1) \to [0, 1]$ is a Hausdorff completion. Consequently, under dependent choice and the ultrafilter lemma, $[0, 1]$ is the Samuel compactification of $(0, 1)$ .

Facts & Assumptions

Given: A real $ε > 0$ and the specified subspace metric uniformities on $(0, 1)$ and $[0, 1]$ .

[L1]

The metric entourages induce the metric topologies and are separated (A metric on a nonempty set generates an entourage uniformity whose induced topology and uniformly continuous maps are the usual metric notions, and this uniformity is separated).

[L2]

There is $m \geq 1$ with $1 / m < ε$ , inverse order reverses on positives, and every real has an integer part (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Inverses of positives are positive, and reciprocation reverses order, Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[L3]

A set is finite when it is equinumerous with a natural number, and total boundedness asks for a finite entourage-ball cover (The cardinality $∣ A ∣$ of a finite set, Totally bounded uniform space).

[L4]

The interval $[0, 1]$ is compact, hence complete for its compatible uniformity (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Every compact uniform space is complete, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

Under dependent choice, the Samuel completion of a separated totally bounded space is its ordinary uniform completion; under the ultrafilter lemma it is compact (Under dependent choice the Samuel completion of a separated totally bounded space is its uniform completion; under the ultrafilter lemma it is compact).

Verification

technique · direct

1.1

Choose $n = m + 1$ , where $m$ is from [L2]; then $n \geq 2$ and $1 / n < ε$ . The map $j \mapsto (j + 1) / n$ is injective on the natural number $m$ , so its image $F = {(j + 1) / n : j \in m}$ is finite and lies in $(0, 1)$ .

L2L3

2.1

For $x \in (0, 1)$ , write $k = ⌊ n x ⌋$ . If $k = 0$ , then $(0 + 1) / n \in F$ is within $1 / n$ of $x$ . Otherwise $1 \leq k < n = m + 1$ , so $k - 1 \in m$ , $k / n \in F$ , and $k / n \leq x < (k + 1) / n$ . Thus $F$ is an $ε$ -net.

L1L2step 1.1

3.1

Hence $(0, 1)$ is separated and totally bounded. The inclusion $i$ pulls back every metric entourage of $[0, 1]$ to the same-radius metric entourage of $(0, 1)$ , and its image is dense because every interval about $0$ , $1$ , or an interior point meets $(0, 1)$ .

L1L3step 2.1

4.1

By [L4], $[0, 1]$ is complete, and by [L1] its metric uniformity is separated; so step 3.1 verifies the completion conditions of A Hausdorff completion of a uniform space and its canonical dense map.

L1L4step 3.1

5.1

The identification in [L5] now gives the Samuel compactification $S ((0, 1)) ≅ [0, 1]$ .

L5step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

Encyclopedia of Mathematics, Uniform space (standard reference, not scraped)