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.

Every continuous $[0, 1]$ -valued function extends uniquely over the closure of the full evaluation image

Statement

Let $e : X \to [0, 1]^{C (X, [0, 1])}$ be the full evaluation map and let $B = \overline{e [X]}$ . Every continuous $g : X \to [0, 1]$ has a unique continuous $\overset{ˉ}{g} : B \to [0, 1]$ with $\overset{ˉ}{g} \circ e = g$ .

Facts & Assumptions

Given: The full evaluation map $e$ , its closure $B$ , and a continuous $g : X \to [0, 1]$ .

[L1]

Coordinate projections from a product are continuous (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

[L2]

Two continuous maps to a Hausdorff target that agree on a dense subset agree everywhere (Two continuous maps into a Hausdorff space that agree on a dense subset are equal).

Proof

technique · direct

1.1

The coordinate projection $π_{g}$ is continuous by [L1]. Its restriction $\overset{ˉ}{g} = π_{g} ∣_{B}$ is continuous and satisfies $\overset{ˉ}{g} (e (x)) = e (x) (g) = g (x)$ .

2.1

If $h : B \to [0, 1]$ is another such extension, then $h$ and $\overset{ˉ}{g}$ agree on $e [X]$ , which is dense in $B$ . Since $[0, 1]$ is Hausdorff, [L2] gives $h = \overset{ˉ}{g}$ .

L2step 1.1∎

Depends on

Used by

Under the ultrafilter lemma and dependent choice, the closure of the full evaluation image is the Stone–Čech compactification Theorem

Dependency tree · two levels

20 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

E. Moorhouse, The Stone–Čech Compactification (standard reference, not scraped)

Every continuous [0,1][0,1]-valued function extends uniquely over the closure of the full evaluation image