CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

Polynomials are uniformly dense in $C([a,b],\mathbb R)$ for every closed interval

Statement

For $a\le b$ , every continuous real function on $[a,b]$ is a uniform limit of polynomials.

Facts & Assumptions

Given: $f\in C([a,b],\mathbb R)$ and $\varepsilon>0$ .

[L1]

Polynomials are uniformly dense on $[0,1]$ (Polynomials are uniformly dense in $C([0,1],\mathbb R)$ ).

[L2]

Closed intervals have the endpoint convention of Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length.

Proof

technique · direct

1.1

If $a=b$ , the constant polynomial $q(x)=f(a)$ agrees with $f$ on the singleton interval.

givenL2algebra

1.2

Now suppose $a<b$ and define $g(t)=f(a+(b-a)t)$ on $[0,1]$ .

givenL2construct

1.3

Choose a polynomial $p$ with $|p(t)-g(t)|<\varepsilon$ on $[0,1]$ by [L1].

L1choose

2.1

Then $q(x)=p((x-a)/(b-a))$ is a polynomial and satisfies $|q(x)-f(x)|<\varepsilon$ on $[a,b]$ . Together with step 1.1 this proves both cases.

step 1.1step 1.2step 1.3algebra∎

Depends on

Used by

The uniform closure of a unital real function algebra is closed under absolute value, maximum, and minimum Lemma

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Bernstein polynomial (Encyclopedia of Mathematics) (standard reference, not scraped)

Polynomials are uniformly dense in C([a,b],R)C([a,b],\mathbb R)C([a,b],R) for every closed interval