# Commit 2021-05-01 20:07 ea379b09

View on Github →feat(topology/continuous_function): the Stone-Weierstrass theorem (#7305)

# The Stone-Weierstrass theorem

If a subalgebra `A`

of `C(X, ℝ)`

, where `X`

is a compact Hausdorff space,
separates points, then it is dense.
We argue as follows.

- In any subalgebra
`A`

of`C(X, ℝ)`

, if`f ∈ A`

, then`abs f ∈ A.topological_closure`

. This follows from the Weierstrass approximation theorem on`[-∥f∥, ∥f∥]`

by approximating`abs`

uniformly thereon by polynomials. - This ensures that
`A.topological_closure`

is actually a sublattice: if it contains`f`

and`g`

, then it contains the pointwise supremum`f ⊔ g`

and the pointwise infimum`f ⊓ g`

. - Any nonempty sublattice
`L`

of`C(X, ℝ)`

which separates points is dense, by a nice argument approximating a given`f`

above and below using separating functions. For each`x y : X`

, we pick a function`g x y ∈ L`

so`g x y x = f x`

and`g x y y = f y`

. By continuity these functions remain close to`f`

on small patches around`x`

and`y`

. We use compactness to identify a certain finitely indexed infimum of finitely indexed supremums which is then close to`f`

everywhere, obtaining the desired approximation. - Finally we put these pieces together.
`L = A.topological_closure`

is a nonempty sublattice which separates points since`A`

does, and so is dense (in fact equal to`⊤`

).

## Future work

Prove the complex version for self-adjoint subalgebras `A`

, by separately approximating
the real and imaginary parts using the real subalgebra of real-valued functions in `A`

(which still separates points, by taking the norm-square of a separating function).
Extend to cover the case of subalgebras of the continuous functions vanishing at infinity,
on non-compact Hausdorff spaces.