LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

The uniform closure of a real function algebra is a vector lattice

Statement

Let $X$ be a compact Hausdorff space and let $A \subseteq C (X, R)$ be a real function algebra, not necessarily unital. Let $\overline{A}$ consist of the continuous functions that can be approximated uniformly by members of $A$ . Then $\overline{A}$ is a real function algebra and a real vector sublattice of $C (X, R)$ .

Facts & Assumptions

Given: A compact Hausdorff space $X$ , a real function algebra $A \subseteq C (X, R)$ , and its uniform closure $\overline{A}$ .

[L1]

For $a \leq b$ , every continuous real function on $[a, b]$ is a uniform limit of polynomials (Polynomials are uniformly dense in $C ([a, b], R)$ for every closed interval).

[L2]

If for every $ε > 0$ a function $f : X \to Y$ has a continuous approximant $g$ with $d (f (x), g (x)) < ε$ for every $x$ , then $f$ is continuous (A uniform limit of continuous functions is continuous, so $C (X, Y)$ is closed in $Y^{X}$ under the uniform metric, clause 1).

[L3]

If $X$ is compact and nonempty and $g : X \to R$ is continuous, then $g [X]$ has a maximum and a minimum (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, clause 2).

[L4]

A real function algebra is a real vector subspace of $C (X, R)$ closed under pointwise multiplication (Unital, point-separating, and nowhere-vanishing real function algebras on a compact Hausdorff space).

Proof

technique · direct

1.1

If $X = \emptyset$ , then $C (X, R)$ consists of the unique empty function, which is the zero element of the vector subspace $A$ ; hence $A = \overline{A} = C (X, R)$ and the claim is immediate.

1.2

Assume $X \neq \emptyset$ . By the definition of uniform closure, every $f \in \overline{A}$ has, for every positive error, a continuous approximant from $A$ , so [L2] confirms that all such uniform limits remain continuous.

L2L4

1.3

The set $\overline{A}$ is a real vector subspace: approximants to $f$ and $g$ add to an approximant to $f + g$ , scalar multiples approximate scalar multiples, and the zero function belongs to $A$ .

L4algebra

2.1

The set $\overline{A}$ is closed under multiplication. Indeed, for $f, g \in \overline{A}$ , [L3] gives finite bounds $M_{f} : = \max_{X} ∣ f ∣$ and $M_{g} : = \max_{X} ∣ g ∣$ . Given $η > 0$ , choose $a, b \in A$ with $∥ a - f ∥_{\infty} < \min {1, η / (2 (M_{g} + 1))}, ∥ b - g ∥_{\infty} < η / (2 (M_{f} + 1)) .$ Then $∣ a ∣ \leq M_{f} + 1$ and $∣ a b - f g ∣ \leq ∣ a ∣ ∣ b - g ∣ + ∣ g ∣ ∣ a - f ∣ < η$ pointwise. Thus products of members of $\overline{A}$ again lie in $\overline{A}$ .

L3L4step 1.3choosealgebra

2.2

Fix $f \in \overline{A}$ and $ε > 0$ . By [L3], $∣ f ∣$ has a maximum $M \geq 0$ ; if $M = 0$ then $f = 0$ and $∣ f ∣ = 0 \in \overline{A}$ .

L3step 1.3

3.1

If $M > 0$ , apply [L1] on $[- M, M]$ to choose a polynomial $q$ with $∣ q (t) - ∣ t ∣ ∣ < ε / 2$ there, and put $p (t) : = q (t) - q (0)$ . Then $p (0) = 0$ , $∣ p (t) - ∣ t ∣ ∣ < ε$ on $[- M, M]$ , and steps 1.3 and 2.1 give $p (f) \in \overline{A}$ . Hence $∣ f ∣$ is uniformly approximable by members of $\overline{A}$ , and therefore belongs to the closed set $\overline{A}$ . Together with the $M = 0$ case in step 2.2, this proves $∣ f ∣ \in \overline{A}$ for every $f \in \overline{A}$ .

L1step 1.3step 2.1step 2.2choosealgebra

4.1

For $f, g \in \overline{A}$ , the pointwise identities $f \lor g = (f + g + ∣ f - g ∣) / 2$ and $f \land g = (f + g - ∣ f - g ∣) / 2$ , together with steps 1.3 and 3.1, put both functions in $\overline{A}$ ; hence $\overline{A}$ is a real vector sublattice.

step 1.3step 3.1algebra∎

Depends on

Used by

Real Stone–Weierstrass theorem for compact Hausdorff spaces Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 114 results over 17 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, Proposition 21.2.4 (standard reference, not scraped)
M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Lemma 9.5 (standard reference, not scraped)
E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, Lemma 1.28 (standard reference, not scraped)