English
For every continuous function on [a,b], there exists a polynomial that approximates it arbitrarily well on [a,b].
Русский
Для любой непрерывной функции на [a,b] существует полином, аппроксимирующий её с любой заданной точностью на [a,b].
LaTeX
$$$\exists p \in \mathbb{R}[X], \forall x \in [a,b],\ |p(x) - f(x)| < \varepsilon.$$$
Lean4
/-- Another alternative statement of Weierstrass's theorem,
for those who like epsilons, but not bundled continuous functions.
Every real-valued function `ℝ → ℝ` which is continuous on `[a,b]`
can be approximated to within any `ε > 0` on `[a,b]` by some polynomial.
-/
theorem exists_polynomial_near_of_continuousOn (a b : ℝ) (f : ℝ → ℝ) (c : ContinuousOn f (Set.Icc a b)) (ε : ℝ)
(pos : 0 < ε) : ∃ p : ℝ[X], ∀ x ∈ Set.Icc a b, |p.eval x - f x| < ε :=
by
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_restrict.mp c⟩
obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
use p
rw [norm_lt_iff _ pos] at b
intro x m
exact b ⟨x, m⟩
