exists_mem_subalgebra_near_continuous_of_separatesPoints

English

As above, for a separating subalgebra A, every real-valued continuous function f on X can be uniformly approximated by elements of A.

Русский

Пусть A разделяет точки; тогда вся функция непрерывна на X может быть аппроксимирована элементами A в норме униформной близости.

LaTeX

$$$\forall f \in C(X, \mathbb{R}), \overline{A} = C(X, \mathbb{R}).$$$

Lean4

/-- An alternative statement of the Stone-Weierstrass theorem,
for those who like their epsilons and don't like bundled continuous functions.

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_continuous_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ)) (w : A.SeparatesPoints)
    (f : X → ℝ) (c : Continuous f) (ε : ℝ) (pos : 0 < ε) : ∃ g : A, ∀ x, ‖(g : X → ℝ) x - f x‖ < ε :=
  by
  obtain ⟨g, b⟩ := exists_mem_subalgebra_near_continuousMap_of_separatesPoints A w ⟨f, c⟩ ε pos
  use g
  rwa [norm_lt_iff _ pos] at b

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