Theorems · Theorem · general topology

ContinuousMapZero.adjoin_id_dense

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : Fact (0 ∈ s)] [CompactSpace ↑s],
  Dense ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id s})

If s : Set 𝕜 with RCLike 𝕜 is compact and contains 0, then the non-unital star subalgebra generated by the identity function in C(s, 𝕜)₀ is dense. This can be seen as a version of the Weierstrass approximation theorem.

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeFactCompactSpace