TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous

Statement

Let $(X, d_{X})$ be a compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space), let $(Y, d_{Y})$ be any metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) and let $f : X \to Y$ be continuous (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). Then $f$ is uniformly continuous (Uniform continuity of a map of metric spaces: one $δ$ serving every point).

No choice principle is used: the cover built below is cut out by a property, and the Lebesgue number lemma it is fed to is itself choice free (Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover).

Facts & Assumptions

Given: A compact metric space $(X, d_{X})$ , a metric space $(Y, d_{Y})$ and a continuous $f : X \to Y$ .

[L1]

$f$ is continuous at $a$ : for every real $ε > 0$ there is a real $δ > 0$ with $f [B_{X} (a, δ)] \subseteq B_{Y} (f (a), ε)$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Open ball, closed ball and sphere in a metric space).

[L2]

$f$ is uniformly continuous when for every real $ε > 0$ there is a real $δ > 0$ such that $d_{X} (x, x^{'}) < δ$ implies $d_{Y} (f (x), f (x^{'})) < ε$ , for all $x, x^{'} \in X$ (Uniform continuity of a map of metric spaces: one $δ$ serving every point).

[L3]

Every open cover of a compact metric space has a Lebesgue number: a real $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies in a single member of the cover (Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover, Open cover, subcover, compact metric space, and compact subset of a metric space).

[L4]

Open balls are open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L5]

For nonempty bounded $A$ , $diam (A) = \sup {d_{X} (u, v) : u, v \in A}$ ; in particular $diam ({x, x^{'}}) = d_{X} (x, x^{'})$ , the set of distances being ${0, d_{X} (x, x^{'})}$ and a metric being nonnegative (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

[L6]

A metric is symmetric and satisfies the triangle inequality (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

Proof

technique · direct

1.1

If $X = \emptyset$ the condition of uniform continuity holds vacuously, so assume $X \neq \emptyset$ , and let $ε > 0$ be real.

2.1

Put $U : = {U \subseteq X : U is open in X and f [U] \subseteq B_{Y} (z, ε / 2) for some z \in Y}$ , a family cut out by a property and not by a selection.

L1step 1.1

3.1

$U$ is an open cover of $X$ : given $x \in X$ , continuity at $x$ supplies a real $δ_{x} > 0$ with $f [B_{X} (x, δ_{x})] \subseteq B_{Y} (f (x), ε / 2)$ , and $B_{X} (x, δ_{x})$ is open and contains $x$ , so it belongs to $U$ .

L1L4step 2.1

4.1

By the Lebesgue number lemma there is a real $δ > 0$ such that every nonempty subset of $X$ of diameter less than $δ$ is contained in a single member of $U$ .

L3step 3.1

5.1

Let $x, x^{'} \in X$ with $d_{X} (x, x^{'}) < δ$ ; the set ${x, x^{'}}$ is nonempty with diameter $d_{X} (x, x^{'}) < δ$ , so ${x, x^{'}} \subseteq U$ for some $U \in U$ , and there is $z \in Y$ with $f [U] \subseteq B_{Y} (z, ε / 2)$ .

L5step 2.1step 4.1

6.1

Then $d_{Y} (f (x), z) < ε / 2$ and $d_{Y} (z, f (x^{'})) < ε / 2$ , so $d_{Y} (f (x), f (x^{'})) \leq d_{Y} (f (x), z) + d_{Y} (z, f (x^{'})) < ε$ ; as $ε > 0$ was arbitrary, $f$ is uniformly continuous.

L2L6step 5.1∎

Remarks

The centre $z$ is not chosen, and that is why the proof is choice free. The family $U$ is defined by the existence of a suitable $z$ , and the argument instantiates that existential once, at step 5.1, for the single member $U$ that the Lebesgue number produced. No function assigning a centre to every member of $U$ is ever needed.

Compactness is not removable. The map $x \mapsto 1 / x$ is continuous on the interval $(0, 1)$ and is not uniformly continuous there ( $x \mapsto 1 / x$ is continuous on $(0, 1)$ and not uniformly continuous, so Heine-Cantor needs compactness of the domain ↗); $(0, 1)$ is not compact.

The codomain is arbitrary. Nothing is assumed about $(Y, d_{Y})$ — not completeness, not boundedness, not compactness. All the work is done on the domain side, which is where the finite subcover lives.

Depends on

Used by

Dependency tree · two levels

34 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

Heine-Cantor theorem (Wikipedia) (standard reference, not scraped)
Lebesgue's number lemma (Wikipedia) (standard reference, not scraped)