Theorems · Theorem · approximation theory

polynomialFunctions_closure_eq_top

∀ (a b : ℝ), (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

The Weierstrass Approximation Theorem: polynomials functions on [a, b] ⊆ ℝ are dense in C([a,b],ℝ) (While we could deduce this as an application of the Stone-Weierstrass theorem, our proof of that relies on the fact that abs is in the closure of polynomials on [-M, M], so we may as well get this done first.)

Defined in

Mathlib.Topology.ContinuousMap.Weierstrass

Cited by

1 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound