theorem weierstrass_approximation {a b : ℝ} (f : C(↑(Set.Icc a b), ℝ)) : ∃ (P : ℕ → Polynomial ℝ), TendstoUniformly (fun (n : ℕ) (x : ↑(Set.Icc a b)) => Polynomial.eval (↑x) (P n)) (⇑f) Filter.atTop

Weierstrass Approximation Theorem. Every continuous real-valued function f on a closed interval [a, b] is the uniform limit of a sequence of polynomials: there exists P : ℕ → ℝ[X] such that Polynomial.eval x (P n) converges to f x uniformly in x ∈ [a, b] as n → ∞.