TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Lattice Stone–Weierstrass theorem on a compact Hausdorff space

Statement

Let $X$ be a compact Hausdorff space and let $L \subseteq C (X, R)$ be a unital point-separating real vector sublattice. Then for every $f \in C (X, R)$ and every $ε > 0$ there is $g \in L$ with $∣ g (x) - f (x) ∣ < ε$ for every $x \in X$ ; that is, $L$ is uniformly dense in $C (X, R)$ . When $X$ is nonempty this is exactly density for the topology of uniform convergence, which Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ defines only on a nonempty domain.

Facts & Assumptions

Given: A compact Hausdorff space $X$ , a unital point-separating real vector sublattice $L \subseteq C (X, R)$ , a target $f \in C (X, R)$ , and a real $ε > 0$ .

[L1]

For distinct $x, y \in X$ and arbitrary $α, β \in R$ , a unital separating real function lattice contains $h$ with $h (x) = α$ and $h (y) = β$ (A unital separating real function lattice interpolates arbitrary values at two distinct points).

[L2]

On a nonempty compact space, a family closed under pointwise maxima and minima and having the two-point duplication property relative to $f$ contains, for every positive error, a member within that error of $f$ at every point (A function lattice with the two-point duplication property uniformly approximates its target).

[L3]

On nonempty $X$ , the topology of uniform convergence on $C (X, R)$ is the metric topology of the restricted uniform metric $\overset{ˉ}{ρ} (f, g) = \sup_{x \in X} \min {∣ f (x) - g (x) ∣, 1}$ (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ ).

Proof

technique · direct

1.1

If $X = \emptyset$ , then $C (X, R)$ contains only the empty function, which is a constant function and hence belongs to the unital lattice $L$ ; the displayed approximation condition holds vacuously, there being no $x$ to test. The topological reading is not asserted here, because [L3] supplies the uniform metric only on a nonempty domain.

L3given

1.2

Assume $X \neq \emptyset$ . For distinct $x, y$ , apply [L1] with $α = f (x)$ and $β = f (y)$ ; for $x = y$ , the constant function with value $f (x)$ belongs to $L$ . Thus $L$ has the two-point duplication property relative to $f$ .

L1given

2.1

Apply [L2] with the positive error $\min {ε, 1} / 2$ to obtain $g \in L$ satisfying $∣ g (x) - f (x) ∣ < \min {ε, 1} / 2 < ε$ for every $x \in X$ .

step 1.2L2

3.1

Suppose further that $X \neq \emptyset$ , which is where [L3] defines the uniform metric. The approximant of step 2.1 then satisfies $\overset{ˉ}{ρ} (f, g) \leq \min {ε, 1} / 2$ , so every uniform-metric neighbourhood of every $f$ meets $L$ ; hence $L$ is dense in the topology of uniform convergence.

step 2.1L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 15 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.3 (standard reference, not scraped)
M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Theorem 9.6, with the vector-space hypothesis used by its proof (standard reference, not scraped)