continuousMap_mem_subalgebra_closure_of_separatesPoints

English

Let A be a separating subalgebra as above. Then for every f in C(X, R) and every ε > 0, there exists g in A such that ∥g − f∥ < ε.

Русский

Пусть A — подалгебра, разделяющая точки. Тогда для всякой f ∈ C(X, R) и любого ε > 0 существует g ∈ A such that ∥g − f∥ < ε.

LaTeX

$$$\forall f \in C(X, \mathbb{R}), \forall \varepsilon>0, \exists g \in A:\; \|g-f\| < \varepsilon.$$$

Lean4

/-- An alternative statement of the Stone-Weierstrass theorem.

If `A` is a subalgebra of `C(X, ℝ)` which separates points (and `X` is compact),
every real-valued continuous function on `X` is a uniform limit of elements of `A`.
-/
theorem continuousMap_mem_subalgebra_closure_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints)
    (f : C(X, ℝ)) : f ∈ A.topologicalClosure :=
  by
  rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]
  simp

Похожие утверждения