Theorem 11.7.16 — Complex non-unital Stone–Weierstrass theorem

Proved

LeblRA.complex_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 complex algebra of continuous complex-valued functions on $X$ , not necessarily containing the constant function $1$ . Suppose that

\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,

and that $A$ is closed under pointwise conjugation:

g\in A\Longrightarrow \overline g\in A.

Then

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

The conclusion gives uniform approximation of every continuous complex-valued function by members of $A$ . This is the full non-unital complex Stone–Weierstrass theorem, Lebl’s Theorem 11.7.16.

Formalization Note. The algebra includes zero but does not assume a unit. Point separation, nowhere-vanishing, and conjugation closure are distinct explicit hypotheses. On continuous complex-valued maps, the Lean star operation is pointwise conjugation. Closure is the uniform closure on the compact domain; empty compact spaces are included.

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 complex_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)
    (adj : ∀ g ∈ A, star g ∈ A) :
    closure (A : Set C(X, ℂ)) = Set.univ := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Theorem 11.7.16. 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.complex_stone_weierstrass

For every type $X$ equipped with a metric whose induced topology is compact, and every complex vector subspace $A$ of the space $C(X,\mathbb C)$ of continuous complex-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)$ , that for every $x\in X$ there exists $g\in A$ such that $g(x)\ne0$ , and that for every $g\in A$ the function $x\mapsto\overline{g(x)}$ also belongs to $A$ , where the bar denotes complex conjugation. Then the topological closure of the underlying set of $A$ equals all of $C(X,\mathbb C)$ . The subspace condition means that $A$ contains the zero function and is closed under addition and multiplication by every complex scalar; membership of the constant function $1$ is not assumed and is not excluded. Conjugation is applied to each function value and does not act on points of $X$ . 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 C$ and every real $\varepsilon>0$ there exists $g\in A$ for which $|f(x)-g(x)|<\varepsilon$ for every $x\in X$ , with complex modulus as the absolute value. The approximating $g$ may depend on $f$ and $\varepsilon$ , and no uniqueness or equality $A=C(X,\mathbb C)$ is asserted. Empty and singleton metric spaces are included: on the empty space the separation and nonvanishing hypotheses are vacuous, and the sole function is fixed by pointwise conjugation; on a singleton separation 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