LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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,\mathcal U)$ is totally bounded, then $\mathcal U=\mathcal U_S$ .

Facts & Assumptions

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

[L1]

The Samuel uniformity is coarser than $\mathcal 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\le1/4\}\subseteq E_1$ ; every set $\{p<\varepsilon\}$ 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 $\mathbb{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)|\le 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)\le 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 $\mathcal U=\mathcal 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 · next 3 levels

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

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