English
If A is a subalgebra of C(X, R) on a compact space X that separates points, then its topological closure (uniform closure) equals all of C(X, R).
Русский
Если A — подалгебра C(X, R) над компактным X, и A разделяет точки, то её топологическое замыкание равно всей C(X, R).
LaTeX
$$$\overline{A} = C(X, \mathbb{R}).$$$
Lean4
/-- 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.
-/
theorem subalgebra_topologicalClosure_eq_top_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints) :
A.topologicalClosure = ⊤ := by
-- The closure of `A` is closed under taking `sup` and `inf`,
-- and separates points strongly (since `A` does),
-- so we can apply `sublattice_closure_eq_top`.
apply SetLike.ext'
let L := A.topologicalClosure
have n : Set.Nonempty (L : Set C(X, ℝ)) := ⟨(1 : C(X, ℝ)), A.le_topologicalClosure A.one_mem⟩
convert
sublattice_closure_eq_top (L : Set C(X, ℝ)) n
(fun f fm g gm => inf_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
(fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
(Subalgebra.SeparatesPoints.strongly (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w))
simp [L]
