Proposition 11.7.6 — Closure preserves real and complex function algebras

Proved

LeblRA.algebra_closure

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

analysis

Let $X$ be a compact metric space. For each of the fields $K=\mathbb R$ and $K=\mathbb C$ , let $A$ be an algebra of continuous $K$ -valued functions on $X$ , not necessarily containing the constant function $1$ . Then

\exists B\subseteq C(X,K),\qquad B\text{ is a }K\text{-algebra}\quad\land\quad B=\overline A,

where closure is taken in the uniform topology.

This is Lebl’s Proposition 11.7.6: uniform closure preserves the algebraic operations. The real and complex assertions are kept together.

Formalization Note. An algebra contains zero and is closed under addition, pointwise multiplication, and multiplication by every scalar. No point separation, nowhere-vanishing, conjugation closure, or prior closedness is assumed. The Lean carrier equality is exactly equality with topological closure in the continuous-function space, whose compact-open and uniform topologies agree here. 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 algebra_closure {X : Type*} [MetricSpace X] [CompactSpace X] :
    (∀ A : NonUnitalSubalgebra ℝ C(X, ℝ),
      ∃ B : NonUnitalSubalgebra ℝ C(X, ℝ), (B : Set C(X, ℝ)) = closure (A : Set C(X, ℝ))) ∧
    (∀ A : NonUnitalSubalgebra ℂ C(X, ℂ),
      ∃ B : NonUnitalSubalgebra ℂ C(X, ℂ), (B : Set C(X, ℂ)) = closure (A : Set C(X, ℂ))) := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Proposition 11.7.6. 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.algebra_closure

For every type $X$ equipped with a metric whose induced topology is compact, both of the following assertions hold: for 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, there exists a real vector subspace $B$ of $C(X,\mathbb R)$ closed under pointwise multiplication whose underlying set is exactly the topological closure of the underlying set of $A$ ; and for 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, there exists a complex vector subspace $B$ of $C(X,\mathbb C)$ closed under pointwise multiplication whose underlying set is exactly the topological closure of the underlying set of $A$ . In each clause a subspace contains the zero function and is closed under addition and multiplication by every scalar in the specified field; it is not required to contain the constant function $1$ , although it may do so. Closure is taken within the stated space of continuous functions in its compact-open topology, which here is the topology of uniform convergence: the equality of sets means that, for each continuous function $f$ in the corresponding space, $f\in B$ if and only if for every real $\varepsilon>0$ there exists $g\in A$ such that $|f(x)-g(x)|<\varepsilon$ for every $x\in X$ , using complex modulus in the complex clause. The two clauses have separately quantified choices of $A$ and $B$ ; $B$ may depend on $A$ , and no explicit uniqueness claim is made. The type $X$ may be empty or a singleton, and $A$ may be the zero subspace or the whole function space; on the empty type there is just one function to either scalar field. There is no assumption that $A$ separates points, has a function nonzero at each point, is already closed, or in the complex case is closed under conjugation, and there is no assertion that its closure is the whole ambient function space.

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