mathlib3

ea379b09 - feat(topology/continuous_function): the Stone-Weierstrass theorem (#7305)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>