English
An ε-approximation statement: if A separates points, then for every continuous f on X and every ε > 0 there exists g in A with ∥g − f∥ < ε.
Русский
Если A разделяет точки, то для каждого непрерывного f на X и любого ε > 0 существует g ∈ A такое, что ∥g − f∥ < ε.
LaTeX
$$$\forall f:\ C(X, \mathbb{R}), \forall \varepsilon>0, \exists g \in A:\; \|g-f\| < \varepsilon.$$$
Lean4
/-- 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`.
-/
theorem exists_mem_subalgebra_near_continuousMap_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints)
(f : C(X, ℝ)) (ε : ℝ) (pos : 0 < ε) : ∃ g : A, ‖(g : C(X, ℝ)) - f‖ < ε :=
by
have w := mem_closure_iff_frequently.mp (continuousMap_mem_subalgebra_closure_of_separatesPoints A w f)
rw [Metric.nhds_basis_ball.frequently_iff] at w
obtain ⟨g, H, m⟩ := w ε pos
rw [Metric.mem_ball, dist_eq_norm] at H
exact ⟨⟨g, m⟩, H⟩
