Theorem 11.7.12 — Real non-unital Stone–Weierstrass theorem

Proved

LeblRA.real_stone_weierstrass

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysis

Let $X$ be a compact metric space, and let $A$ be a real algebra of continuous real-valued functions on $X$ , not necessarily containing the constant function $1$ . Assume

\forall x\ne y\;\exists g\in A,\quad g(x)\ne g(y), \qquad \forall x\in X\;\exists g\in A,\quad g(x)\ne0.

Then

\overline A=C(X,\mathbb R).

Equivalently, for every $f\in C(X,\mathbb R)$ and every $\varepsilon>0$ , some $g\in A$ satisfies $|g(x)-f(x)|<\varepsilon$ for all $x\in X$ . This is the real non-unital density result in Lebl’s Theorem 11.7.12.

Formalization Note. The algebra contains zero and is closed under addition, multiplication, and real scalar multiplication. Nowhere-vanishing remains an explicit hypothesis; no single everywhere nonzero element is assumed. Closure is taken in the continuous-function space, where compact-open and uniform convergence agree. Empty compact spaces are allowed.

Preamble

import Mathlib.Topology.ContinuousMap.StoneWeierstrass
import Mathlib.Topology.Algebra.NonUnitalAlgebra
import Mathlib.Analysis.Complex.Basic

set_option autoImplicit false
open Set Filter Topology
open scoped ContinuousMapZero
open scoped Polynomial

Formal statement

namespace LeblRA
theorem real_stone_weierstrass {X : Type*} [MetricSpace X] [CompactSpace X]
    (A : NonUnitalSubalgebra ℝ C(X, ℝ))
    (sep : ∀ x y : X, x ≠ y → ∃ g ∈ A, g x ≠ g y)
    (nv : ∀ x : X, ∃ g ∈ A, g x ≠ 0) :
    closure (A : Set C(X, ℝ)) = Set.univ := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Theorem 11.7.12. Author-hosted HTML: https://www.jirka.org/ra/html/sec_stoneweier.html (accessed 2026-09-05). The algebra conventions are Definitions 11.7.5, 11.7.7, and 11.7.15; no unit is assumed.

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

Declaration: LeblRA.real_stone_weierstrass

For every type $X$ equipped with a metric whose induced topology is compact, and every real vector subspace $A$ of the space $C(X,\mathbb R)$ of continuous real-valued functions on $X$ that is closed under pointwise multiplication, suppose that for every $x,y\in X$ with $x\ne y$ there exists $g\in A$ such that $g(x)\ne g(y)$ , and that for every $x\in X$ there exists $g\in A$ such that $g(x)\ne0$ . Then the topological closure of the underlying set of $A$ equals all of $C(X,\mathbb R)$ . The subspace condition means that $A$ contains the zero function and is closed under addition and multiplication by every real scalar; membership of the constant function $1$ is not assumed and is not excluded. The point-separating function may depend on the pair of distinct points, and the nonvanishing function may depend on the point; neither hypothesis requires a single common witness. Closure is within the continuous function space with its compact-open topology, which here is the topology of uniform convergence, so the conclusion says that for every continuous $f:X\to\mathbb R$ and every real $\varepsilon>0$ there exists $g\in A$ for which $|f(x)-g(x)|<\varepsilon$ for every $x\in X$ . The approximating $g$ may depend on $f$ and $\varepsilon$ , and no uniqueness or equality $A=C(X,\mathbb R)$ is asserted. Empty and singleton metric spaces are included: on the empty space both hypotheses are vacuous and the continuous function space has one element; on a singleton the separation hypothesis is vacuous but the nonvanishing hypothesis still requires a function nonzero at its point. On any nonempty $X$ , the zero subspace does not satisfy the nonvanishing hypothesis.

Readback model identifier: unavailable; no actual runtime model identifier was supplied to this auditor.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph