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.

The evaluation map of a point–closed-set separating family is a topological embedding

Statement

If a family $F$ separates points from closed sets (A family of continuous unit-interval-valued functions that separates points from closed sets), then its evaluation map $e_{F}$ (The evaluation map from a space into the unit cube indexed by a family of continuous functions) is a homeomorphism of $X$ onto the subspace $e_{F} [X]$ . In particular it is a topological embedding.

Facts & Assumptions

Given: A space $X$ , a point–closed-set separating family $F$ , and its evaluation map $e = e_{F}$ .

[L1]

A map into a product is continuous exactly when all of its coordinate maps 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]

A homeomorphism is a bijection whose map and inverse are continuous (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Proof

technique · direct

1.1

Each coordinate $π_{f} \circ e$ equals $f$ and is continuous, so $e$ is continuous by [L1].

1.2

If $x \neq y$ , point separation supplies $f \in F$ with $f (x) \neq f (y)$ , and then $e (x) (f) \neq e (y) (f)$ . Thus $e$ is injective.

given

1.3

Let $U$ be open in $X$ and $x \in U$ . The complement $C = X ∖ U$ is closed, so choose $f \in F$ with $f (x) = 1$ and $f [C] = {0}$ . Then $e (x)$ belongs to $e [X] \cap π_{f}^{- 1} ((1 / 2, 1])$ , and this subspace-open set is contained in $e [U]$ .

givenconstruct

2.1

Step 1.3 shows that $e [U]$ is open in $e [X]$ for every open $U$ , so $e^{- 1} : e [X] \to X$ is continuous. Together with step 1.1 and injectivity from step 1.2, [L2] proves the assertion.

step 1.1step 1.2step 1.3L2∎

Depends on

Used by

A space is Tychonoff if and only if it embeds in a cube [0,1]^J Theorem
Banach-Stone Theorem

Dependency tree · two levels

17 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)