Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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⊆C(X,R) be a real function algebra, not necessarily unital. Let A‾ consist of the continuous functions that can be approximated uniformly by members of A. Then 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⊆C(X,R), and its uniform closure A‾.

[L1]

For a≤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→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 YX under the uniform metric, clause 1).

[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.1L4

If X=∅, then C(X,R) consists of the unique empty function, which is the zero element of the vector subspace A; hence A=A‾=C(X,R) and the claim is immediate.

1.2L2L4

Assume X≠∅. By the definition of uniform closure, every f∈A‾ has, for every positive error, a continuous approximant from A, so [L2] confirms that all such uniform limits remain continuous.

1.3L4algebra

The set 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.

2.1L3L4step 1.3choosealgebra

The set A‾ is closed under multiplication. Indeed, for f,g∈A‾, [L3] gives finite bounds Mf:=max⁡X∣f∣ and Mg:=max⁡X∣g∣. Given η>0, choose a,b∈A with ∥a−f∥∞<min⁡{1,η/(2(Mg+1))},∥b−g∥∞<η/(2(Mf+1)). Then ∣a∣≤Mf+1 and ∣ab−fg∣≤∣a∣∣b−g∣+∣g∣∣a−f∣<η pointwise. Thus products of members of A‾ again lie in A‾.

2.2L3step 1.3

Fix f∈A‾ and ε>0. By [L3], ∣f∣ has a maximum M≥0; if M=0 then f=0 and ∣f∣=0∈A‾.

3.1L1step 1.3step 2.1step 2.2choosealgebra

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)∈A‾. Hence ∣f∣ is uniformly approximable by members of A‾, and therefore belongs to the closed set A‾. Together with the M=0 case in step 2.2, this proves ∣f∣∈A‾ for every f∈A‾.

4.1step 1.3step 3.1algebra∎

For f,g∈A‾, the pointwise identities f∨g=(f+g+∣f−g∣)/2 and f∧g=(f+g−∣f−g∣)/2, together with steps 1.3 and 3.1, put both functions in A‾; hence A‾ is a real vector sublattice.

Depends on

Used by

Dependency tree · two levels

43 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