English
Given a continuous function on a compact interval, for any ε > 0 there exists a polynomial p such that the uniform distance between p and the function is less than ε.
Русский
Для любой ε > 0 существует полином p, который аппроксимирует непрерывную функцию на [a,b] до точности ε по норме максимума.
LaTeX
$$$\exists p \in \mathbb{R}[X], \|p^{\to C([a,b])} - f\|_{\infty} < \varepsilon.$$$
Lean4
/-- 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.
-/
theorem exists_polynomial_near_continuousMap (a b : ℝ) (f : C(Set.Icc a b, ℝ)) (ε : ℝ) (pos : 0 < ε) :
∃ p : ℝ[X], ‖p.toContinuousMapOn _ - f‖ < ε :=
by
have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)
rw [Metric.nhds_basis_ball.frequently_iff] at w
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos
rw [Metric.mem_ball, dist_eq_norm] at H
exact ⟨m, H⟩
