Real Stone--Weierstrass theorem for compact metric spaces

Put $\delta =\epsilon \mathrm{/}3$. For a fixed $x\in K$, let $A_x=\{a\in A:a(x)=f(x)\}$. The open sets $U_a=\{z:a(z)>f(z)-\delta \}$ indexed by all $a\in A_x$ cover $K$: for each $y\mathrm{\ne }x$, [L2] gives one $a\in A_x$ with $a(y)=f(y)$, and the constant $f(x)\mathbf{1}$ handles $y=x$. This asserts existence separately at each point without selecting an interpolant for every pair.

By [L3] this cover has a finite subcover. Choose representatives $a_1,\dots ,a_r\in A_x$ for its finitely many members; $r\ge 1$ since $K$ is nonempty. Their maximum $g={\max }_j{a}_j$ lies in $\bar{A}$ by [L1], satisfies $g(x)=f(x)$, and is greater than $f-\delta$ throughout $K$. This proves existence of such a finite maximum for every fixed $x$; it does not select a family $(g_x{)}_{x\in K}$.

Let $\mathcal{G}$ be the set of all finite nonempty maxima of members of $A$ which satisfy $g>f-\delta$ everywhere on $K$. Every member of $\mathcal{G}$ belongs to $\bar{A}$ and is continuous by [L1]. The open sets $V_g=\{z:g(z)<f(z)+\delta \}$ indexed by all $g\in \mathcal{G}$ cover $K$: for each $x$, the existential conclusion of step 2.1 supplies a member with $g(x)=f(x)$. Thus this second cover also requires no choice indexed by $K$.

By [L3] take a finite subcover and representatives $g_1,\dots ,g_s\in \mathcal{G}$, where $s\ge 1$. Then $h={\min }_i{g}_i\in \bar{A}$ by [L1]. Every $g_i>f-\delta$ globally, and the subcover supplies at each point an index with $g_i<f+\delta$. Hence $f-\delta <h<f+\delta$ pointwise and $\mathrm{\parallel }h-f{\mathrm{\parallel }}_{\mathrm{\infty }}\le \delta$. Only finitely many representatives were selected in either compactness step.

Since $h\in \bar{A}$, choose one $a\in A$ with $\mathrm{\parallel }a-h{\mathrm{\parallel }}_{\mathrm{\infty }}<\delta$. Then $\mathrm{\parallel }a-f{\mathrm{\parallel }}_{\mathrm{\infty }}<2\delta <\epsilon$. For every $f$ and positive target error this gives an approximant in $A$ itself, proving density without any countable or arbitrary-index choice assumption.