Alphabeta MathApproximation and Compactness in
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.
✓ 16 results · all verified · 0 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 16 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Linear Algebra
Real Analysis
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- Topology of ℝ
Set Theory
2 · Logical flowchart
3 · Items
Definition
Equicontinuity, pointwise boundedness, and uniform boundedness for families in C(K,ℝ)
Lemma
An equicontinuous family on a compact metric space is uniformly equicontinuous
Lemma
Equicontinuity and pointwise boundedness on a compact metric space imply uniform boundedness
Lemma
An equicontinuous pointwise-bounded family in C(K,ℝ) has a finite net in the supremum metric
Lemma
A uniformly convergent sequence of continuous functions, together with its limit, is equicontinuous
Theorem
Arzelà--Ascoli for real C(K) under Countable Choice and Dependent Choice: compact closure iff equicontinuous and pointwise bounded
Corollary
Every pointwise-bounded equicontinuous sequence in C(K,ℝ) has a uniformly convergent subsequence
Definition
The Bernstein polynomial Bₙ(f) on [0,1]
Lemma
The zeroth, first, and second centred moments of the Bernstein basis
Theorem
Bernstein polynomials converge uniformly to every continuous function on [0,1]
Corollary
Polynomials are uniformly dense in C([0,1],ℝ)
Corollary
Polynomials are uniformly dense in C([a,b],ℝ) for every closed interval
Definition
A unital point-separating real subalgebra of C(K,ℝ)
Lemma
The uniform closure of a unital real function algebra is closed under absolute value, maximum, and minimum
Lemma
A unital separating real function algebra interpolates arbitrary values at two distinct points
Theorem
Real Stone--Weierstrass theorem for compact metric spaces
Theorem
Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior
Lemma
Functions satisfying a fixed local Lipschitz bound somewhere form a closed subset of C([0,1])
Lemma
Polygonal functions with sufficiently steep nonvertex slopes are dense in C([0,1])
Theorem
Under Dependent Choice, continuous nowhere differentiable functions form a dense subset of C([0,1],ℝ)
Definition
The tent function φ(t)=dist(t,ℤ) and the Takagi series T(x)=∑_n≥02⁻ⁿφ(2ⁿ x)
Theorem