TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Real Stone--Weierstrass theorem for compact metric spaces

Statement

Let $K$ be a nonempty compact metric space and let $A \subseteq C (K, R)$ be a unital subalgebra which separates points. Then $A$ is dense in $C (K, R)$ for the supremum metric.

Facts & Assumptions

Given: $f \in C (K, R)$ and $ε > 0$ .

[L1]

The uniform closure $\overline{A}$ is closed under pointwise maximum and minimum (The uniform closure of a unital real function algebra is closed under absolute value, maximum, and minimum).

[L2]

For distinct $x, y \in K$ and prescribed real values at $x, y$ , $A$ contains a function taking those two values (A unital separating real function algebra interpolates arbitrary values at two distinct points).

[L3]

Every open cover of the compact metric space $K$ has a finite subcover (Open cover, subcover, compact metric space, and compact subset of a metric space).

Proof

technique · constructive

1.1

For fixed $x, y \in K$ , choose $u_{x, y} \in A$ with $u_{x, y} (x) = f (x)$ and $u_{x, y} (y) = f (y)$ , using $f (x) 1$ when $x = y$ and [L2] otherwise.

L2algebra

2.1

For fixed $x$ , the open sets $U_{x, y} = {z : u_{x, y} (z) > f (z) - ε}$ cover $K$ , since $y \in U_{x, y}$ . Select $y_{1}, \dots, y_{r}$ whose sets cover $K$ by [L3].

step 1.1L3construct

3.1

Put $g_{x} = \max_{j} u_{x, y_{j}} \in \overline{A}$ . Then $g_{x} (x) = f (x)$ and $g_{x} > f - ε$ on $K$ .

L1step 2.1algebra

4.1

The open sets $V_{x} = {z : g_{x} (z) < f (z) + ε}$ cover $K$ . By [L3], choose $x_{1}, \dots, x_{s}$ whose $V_{x_{i}}$ cover $K$ .

step 3.1L3construct

5.1

The function $h = \min_{i} g_{x_{i}}$ belongs to $\overline{A}$ by [L1], and $f - ε < h < f + ε$ pointwise. Thus $∥ h - f ∥_{\infty} < ε$ .

L1step 3.1step 4.1algebra

6.1

Since $ε$ was arbitrary and every $h$ of step 5.1 lies in the closed set $\overline{A}$ , the function $f$ lies in $\overline{A}$ . Thus $\overline{A} = C (K, R)$ and $A$ is dense.

step 5.1discharge-construct∎

Depends on

Used by

Dependency tree · two levels

12 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

Stone-Weierstrass Theorem (University of Chicago) (standard reference, not scraped)