Theorems · Theorem · approximation theory

exists_polynomial_near_continuousMap

∀ (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)) (ε : ℝ), 0 < ε → ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

An alternative statement of Weierstrass' theorem, for those who like their epsilons. Every real-valued continuous function on [a,b] is within any ε > 0 of some polynomial.

Defined in

Mathlib.Topology.ContinuousMap.Weierstrass

Cited by

1 results in Mathlib

Foundations

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