LemmaStatement: AI-adaptedProof: 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.

Assuming dependent choice, a totally bounded uniformity equals its Samuel uniformity

Statement

Assume dependent choice. If $(X, U)$ is totally bounded, then $U = U_{S}$ .

Facts & Assumptions

Given: A totally bounded uniform space $(X, U)$ , dependent choice, and an entourage $U \in U$ .

[L1]

The Samuel uniformity is coarser than $U$ (Samuel function pseudometrics generate a uniformity coarser than the original one).

[L2]

Under dependent choice there is a normal symmetric sequence with $E_{1} \subseteq U$ , and its controlled pseudometric $p$ satisfies ${p \leq 1 / 4} \subseteq E_{1}$ ; every set ${p < ε}$ is an original entourage, so $p$ is uniformly continuous (Assuming dependent choice, every entourage admits a normal symmetric sequence subordinate to it, A normal sequence of entourages yields a uniformly continuous pseudometric with controlled dyadic balls, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L3]

Total boundedness supplies a finite set $F \subseteq X$ whose ${p < 1 / 16}$ -balls cover $X$ (Totally bounded uniform space).

Proof

technique · constructive

1.1

By [L1], it is enough to show that every original entourage contains a Samuel entourage.

1.2

Take $p$ as in [L2] and a finite $p$ -net $F$ as in [L3]; for $z \in F$ put $f_{z} (y) = \min {1, p (z, y)}$ .

L2L3construct

2.1

Each $f_{z}$ is $[0, 1]$ -valued and uniformly continuous: the pseudometric triangle inequality gives $∣ p (z, x) - p (z, y) ∣ \leq p (x, y)$ , and truncation at $1$ does not increase this difference. Thus every $f_{z}$ is a Samuel coordinate.

L2step 1.2

3.1

If $∣ f_{z} (x) - f_{z} (y) ∣ < 1 / 8$ for every $z \in F$ , choose $z \in F$ with $p (z, x) < 1 / 16$ . Then $f_{z} (x) = p (z, x) < 1 / 16$ and $f_{z} (y) < 3 / 16 < 1$ , so $p (z, y) = f_{z} (y)$ ; hence $p (x, y) \leq p (x, z) + ∣ f_{z} (x) - f_{z} (y) ∣ + p (z, x) < 1 / 16 + 1 / 8 + 1 / 16 = 1 / 4$ .

L3step 1.2step 2.1

4.1

The finite-coordinate Samuel entourage in step 3.1 lies in ${p < 1 / 4} \subseteq U$ , so step 1.1 proves $U = U_{S}$ ; the empty space is immediate.

L1L2step 3.1discharge-construct∎

Depends on

Used by

Under dependent choice the Samuel completion of a separated totally bounded space is its uniform completion; under the ultrafilter lemma it is compact Corollary

Dependency tree · two levels

35 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

M. Megrelishvili, Samuel and Smirnov compactifications (standard reference, not scraped)