English
Let A separate points in X. For any continuous f on X and any compact K ⊆ X and ε > 0, there exists g ∈ A with sup_{x∈K} |g(x) − f(x)| < ε.
Русский
Пусть A разделяет точки в X. Для любого непрерывного f на X и любого компактного K ⊆ X и ε > 0 найдется g ∈ A такое, что sup_{x∈K} |g(x) − f(x)| < ε.
LaTeX
$$$\exists g \in A:\; \sup_{x\in K} |g(x)-f(x)| < \varepsilon.$$$
Lean4
/-- A variant of the Stone-Weierstrass theorem where `X` need not be compact:
If `A` is a subalgebra of `C(X, ℝ)` which separates points, then, for any compact set `K ⊆ X`,
every real-valued continuous function on `X` is within any `ε > 0` of some element of `A` on `K`. -/
theorem exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints {X : Type*} [TopologicalSpace X]
{A : Subalgebra ℝ C(X, ℝ)} (hA : A.SeparatesPoints) (f : C(X, ℝ)) {K : Set X} (hK : IsCompact K) {ε : ℝ}
(pos : 0 < ε) : ∃ g ∈ A, ∀ x ∈ K, ‖(g : X → ℝ) x - f x‖ < ε :=
by
let restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(K, ℝ) :=
ContinuousMap.compStarAlgHom' ℝ ℝ
⟨(Subtype.val), continuous_subtype_val⟩
--consider the subalgebra AK of functions with domain K
let AK : Subalgebra ℝ C(K, ℝ) := Subalgebra.map (restrict_on_K) A
have hsep : AK.SeparatesPoints := by
intro x y hxy
obtain ⟨_, ⟨g, hg1, hg2⟩, hg_sep⟩ := hA (Subtype.coe_ne_coe.mpr hxy)
simp only [Set.mem_image, SetLike.mem_coe, exists_exists_and_eq_and]
use restrict_on_K g
refine
⟨Subalgebra.mem_map.mpr ?_, by simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]⟩
use g, hg1
simp [AlgHom.coe_coe]
obtain ⟨⟨gK, hgKAK⟩, hgapprox⟩ :=
@ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints _ _ (isCompact_iff_compactSpace.mp hK) AK
hsep (K.restrict f) (ContinuousOn.restrict (Continuous.continuousOn f.continuous)) ε pos
obtain ⟨g, hgA, hgKAK⟩ := Subalgebra.mem_map.mp hgKAK
use g, hgA
intro x hxK
have eqg : g x = gK ⟨x, hxK⟩ := by rw [← hgKAK]; rfl
rw [eqg]
exact hgapprox ⟨x, hxK⟩
