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.

Total boundedness passes to a uniform space with a dense uniformly continuous image

Statement

Let $i:X\to Y$ be uniformly continuous with dense image. If $X$ is totally bounded, then $Y$ is totally bounded.

Facts & Assumptions

Given: A target entourage $E$ of $Y$ , a uniformly continuous map $i:X\to Y$ with dense image, and a totally bounded source $X$ .

[L1]

The uniformity square-root axiom gives $D$ with $D\circ D\subseteq E$ ; a symmetric-entourage base then gives symmetric $V\subseteq D$ , hence $V\circ V\subseteq E$ (Uniform space in the entourage formulation, Every uniformity has a base of symmetric entourages).

[L2]

Uniform continuity supplies a source entourage $U$ whose $U$ -related pairs have $V$ -related images (Uniformly continuous map between uniform spaces).

[L3]

Total boundedness supplies a finite $F\subseteq X$ with $X=\bigcup_{a\in F}U[a]$ (Totally bounded uniform space).

[L4]

Entourage balls are neighbourhoods, so density makes every nonempty target entourage ball meet $i[X]$ (The sets containing an entourage ball about each of their points form a topology).

Proof

technique · direct

1.1

Choose $V$ and $U$ as in [L1] and [L2], and choose the finite $U$ -net $F$ from [L3].

L1L2L3

1.2

For $y\in Y$ , density gives $x\in X$ with $i(x)\in V[y]$ ; choose $a\in F$ with $x\in U[a]$ .

L3L4

2.1

Step 1.2 gives $(i(a),i(x))\in V$ and, by symmetry, $(i(x),y)\in V$ , hence $(i(a),y)\in V\circ V\subseteq E$ .

step 1.1step 1.2

3.1

The finite set $i[F]$ has $E$ -balls covering $Y$ , proving total boundedness; if $Y=\varnothing$ , the empty set is the required finite net.

L3step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

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

J. Wodzicki, Uniform Structure (standard reference, not scraped)