starClosure_topologicalClosure — Mathlib

English

The star subalgebra generated by polynomial functions is dense in C(s, 𝕜) when s is compact and 𝕜 ∈ {ℝ, ℂ}.

Русский

Звёздная подалгебра, порожденная полиномами, плотна в C(s, 𝕜) при s компактно и 𝕜 ∈ {ℝ, ℂ}.

LaTeX

$$$((\text{polynomialFunctions}(s)).\text{starClosure}).\text{topologicalClosure} = \top.$$$

Lean4

/-- The star subalgebra generated by polynomials functions is dense in `C(s, 𝕜)` when `s` is
compact and `𝕜` is either `ℝ` or `ℂ`. -/
theorem starClosure_topologicalClosure {𝕜 : Type*} [RCLike 𝕜] (s : Set 𝕜) [CompactSpace s] :
    (polynomialFunctions s).starClosure.topologicalClosure = ⊤ :=
  ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
    (Subalgebra.separatesPoints_monotone le_sup_left (polynomialFunctions_separatesPoints s))

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