Theorem 7.32 — Stone–Weierstrass

Disproved

Rudin.ch07_stone_weierstrass

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisapproximationtopology

Let $\mathcal{A}$ be an algebra of real continuous functions on a compact set $K$ . If $\mathcal{A}$ separates points on $K$ and vanishes at no point of $K$ , then every real continuous function on $K$ lies in the uniform closure of $\mathcal{A}$ : it is the uniform limit on $K$ of a sequence of members of $\mathcal{A}$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 7.32 (Stone–Weierstrass): let `A` be an algebra of real continuous functions
on a compact set `K`.  If `A` separates points on `K` and vanishes at no point of `K`, then
the uniform closure of `A` on `K` contains every function that is continuous on `K`. -/
theorem ch07_stone_weierstrass {X : Type*} [MetricSpace X] (K : Set X) (hK : IsCompact K)
    (A : Set (X → ℝ)) (halg : IsFunctionAlgebra A) (hcont : ∀ f ∈ A, ContinuousOn f K)
    (hsep : SeparatesPointsOn A K) (hvan : VanishesAtNoPointOn A K) :
    ∀ g : X → ℝ, ContinuousOn g K → g ∈ UniformClosureOn A K := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7, p. 162, Theorems 7.29, 7.31 and 7.32

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $X$ be a metric space and $K \subseteq X$ compact. Let $A$ be a set of real-valued functions on $X$ such that:

$A$ is an algebra: closed under pointwise sums, pointwise products, and multiplication by real scalars;
every $f \in A$ is continuous on $K$ (relative continuity; the members of $A$ are functions on all of $X$ but only their behaviour on $K$ is constrained);
$A$ separates points on $K$ : for all $x,y \in K$ with $x \ne y$ there is $f \in A$ with $f(x) \ne f(y)$ ;
$A$ vanishes at no point of $K$ : for every $x \in K$ there is $f \in A$ with $f(x) \ne 0$ .

Then for every function $g : X \to \mathbb{R}$ that is continuous on $K$ , $g$ belongs to the uniform closure of $A$ on $K$ — that is, there exists a sequence $f_0,f_1,\dots$ of members of $A$ with $f_n \to g$ uniformly on $K$ .

The conclusion constrains $g$ only through uniform approximation on $K$ ; the approximating functions agree with $g$ nowhere in particular off $K$ . $K$ may be empty, in which case every $g$ trivially qualifies.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph