# The Stone-Weierstrass theorem #

If a subalgebra `A`

of `C(X, ℝ)`

, where `X`

is a compact topological 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.topologicalClosure`

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

by approximating`abs`

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

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.topologicalClosure`

is a nonempty sublattice which separates points since`A`

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

).

We then prove the complex version for star 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).

## Future work #

Extend to cover the case of subalgebras of the continuous functions vanishing at infinity, on non-compact spaces.

Given a continuous function `f`

in a subalgebra of `C(X, ℝ)`

, postcomposing by a polynomial
gives another function in `A`

.

This lemma proves something slightly more subtle than this:
we take `f`

, and think of it as a function into the restricted target `Set.Icc (-‖f‖) ‖f‖)`

,
and then postcompose with a polynomial function on that interval.
This is in fact the same situation as above, and so also gives a function in `A`

.

The **Stone-Weierstrass Approximation Theorem**,
that a subalgebra `A`

of `C(X, ℝ)`

, where `X`

is a compact topological space,
is dense if it separates points.

An alternative statement of the Stone-Weierstrass theorem.

If `A`

is a subalgebra of `C(X, ℝ)`

which separates points (and `X`

is compact),
every real-valued continuous function on `X`

is a uniform limit of elements of `A`

.

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons.

If `A`

is a subalgebra of `C(X, ℝ)`

which separates points (and `X`

is compact),
every real-valued continuous function on `X`

is within any `ε > 0`

of some element of `A`

.

An alternative statement of the Stone-Weierstrass theorem, for those who like their epsilons and don't like bundled continuous functions.

If `A`

is a subalgebra of `C(X, ℝ)`

which separates points (and `X`

is compact),
every real-valued continuous function on `X`

is within any `ε > 0`

of some element of `A`

.

If a star subalgebra of `C(X, 𝕜)`

separates points, then the real subalgebra
of its purely real-valued elements also separates points.

The Stone-Weierstrass approximation theorem, `IsROrC`

version, that a star subalgebra `A`

of
`C(X, 𝕜)`

, where `X`

is a compact topological space and `IsROrC 𝕜`

, is dense if itseparates
points.

Polynomial functions in are dense in `C(s, ℝ)`

when `s`

is compact.

See `polynomialFunctions_closure_eq_top`

for the special case `s = Set.Icc a b`

which does not use
the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as
well.

The star subalgebra generated by polynomials functions is dense in `C(s, 𝕜)`

when `s`

is
compact and `𝕜`

is either `ℝ`

or `ℂ`

.

Continuous algebra homomorphisms from `C(s, ℝ)`

into an `ℝ`

-algebra `A`

which agree
at `X : 𝕜[X]`

(interpreted as a continuous map) are, in fact, equal.

Continuous star algebra homomorphisms from `C(s, 𝕜)`

into a star `𝕜`

-algebra `A`

which agree
at `X : 𝕜[X]`

(interpreted as a continuous map) are, in fact, equal.