Alphabeta MathStone–Weierstrass in General
About this page
How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
✓ 13 results · all verified · 10 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
- Binary Operations, Monoids, Groups and Subgroups
- Cosets, Index and Lagrange's Theorem
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Normal Subgroups and Quotient Groups
- Polynomial Rings, the Division Algorithm and Roots
- Rings, Subrings, Integral Domains and Fields
- Simple Field Extensions and the Construction of the Complex Numbers
Linear Algebra
Real Analysis
- Approximation and Compactness in C(K)
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Suprema and Infima
- The Complex Exponential and Euler's Formula
Set Theory
2 · Logical flowchart
3 · Items
Definition
The two-point duplication property of a function family relative to a target function
Definition
Unital point-separating real vector sublattices of C(X,ℝ)
Definition
Unital, point-separating, and nowhere-vanishing real function algebras on a compact Hausdorff space
Definition
Self-adjoint complex function algebras, unitality, and point separation
Proposition
The general real function-algebra definition agrees with the published compact-metric definition
Lemma
A unital separating real function lattice interpolates arbitrary values at two distinct points
Lemma
A function lattice with the two-point duplication property uniformly approximates its target
Theorem
Lattice Stone–Weierstrass theorem on a compact Hausdorff space
Lemma
The uniform closure of a real function algebra is a vector lattice
Theorem
Real Stone–Weierstrass theorem for compact Hausdorff spaces
Lemma
A nowhere-vanishing real function algebra on a compact space approximates the constant one
Theorem
A separating real function algebra is dense or its closure consists exactly of the functions vanishing at one point
Corollary
A point-separating nowhere-vanishing real function algebra is uniformly dense
Lemma
The real-valued part of a point-separating self-adjoint complex function algebra is separating and has the same common zeros
Theorem
Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense
Corollary
The unital algebra generated by a separating complex family and its conjugates is dense
Definition
The quotient that identifies points indistinguishable by a real function algebra
Theorem
A closed unital real function algebra is C(Y,ℝ) on its indistinguishability quotient
Sources
- J. M. Erdman, A Companion to Real Analysis, Definition 21.2.2
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, Lemma 1.27
- M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Definition 9.4 and Theorem 9.6
- J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.3
- J. M. Erdman, A Companion to Real Analysis, Section 21.2
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, Theorem 1.26
- J. M. Erdman, A Companion to Real Analysis, Definition 21.2.13
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, definition preceding Theorem 1.29
- J. M. Erdman, A Companion to Real Analysis, Proposition 21.2.5
- M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Theorem 9.6, with the vector-space hypothesis used by its proof
- J. M. Erdman, A Companion to Real Analysis, Proposition 21.2.4
- M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Lemma 9.5
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, Lemma 1.28
- J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.6
- M. Xu, Math 205B notes from a course by R. Mazzeo (Stanford), Theorem 9.3
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, proof of Theorem 1.26
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, consequence of Theorem 1.26
- J. M. Erdman, A Companion to Real Analysis, proof of Theorem 21.2.14
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, proof of Theorem 1.29
- J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.14
- E. Carlen, Notes on Topology and the Stone-Weierstrass Theorem, Theorem 1.29
- J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.15