theorem Weierstrass.weierstrass_approximation (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc 0 1)) (ε : ℝ) (hε : 0 < ε) : ∃ (p : Polynomial ℝ), ∀ x ∈ Set.Icc 0 1, |Polynomial.eval x p - f x| ≤ ε

Weierstrass approximation theorem (Theorem 4.7.1, 1885). Every continuous function $f : [0, 1] \to \mathbb{R}$ can be uniformly approximated by polynomials: for every $\varepsilon > 0$ there exists a polynomial $p \in \mathbb{R}[X]$ such that $|p(x) - f(x)| \le \varepsilon$ for all $x \in [0, 1]$.