topologicalClosure — Mathlib

English

Polynomial functions in are dense in C(s, ℝ) when s is compact.

Русский

Полиномиальные функции в плотны в C(s, ℝ), если s компактно.

LaTeX

$$$\overline{\text{polynomialFunctions}(s)} = C(s, \mathbb{R}).$$$

Lean4

/-- Polynomial functions in are dense in `C(s, ℝ)` when `s` is compact.

See `polynomialFunctions_closure_eq_top` for the special case `s = Set.Icc a b` which does not use
the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as
well. -/
theorem topologicalClosure (s : Set ℝ) [CompactSpace s] : (polynomialFunctions s).topologicalClosure = ⊤ :=
  ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints _ (polynomialFunctions_separatesPoints s)

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