Theorems · Theorem · general topology

ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints

∀ {𝕜 : Type u_1} {X : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  (A : StarSubalgebra 𝕜 C(X, 𝕜)), A.SeparatesPoints → A.topologicalClosure = ⊤

The Stone-Weierstrass approximation theorem, RCLike version, that a star subalgebra A of C(X, 𝕜), where X is a compact topological space and RCLike 𝕜, is dense if it separates points.

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

4 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeTopologicalSpaceCompactSpace