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.

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 = ⋃_{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 = \emptyset$ , the empty set is the required finite net.

L3step 2.1∎

Depends on

Used by

Dependency tree · two levels

11 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

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