Stone–Weierstrass (intervals)

import Mathlib

theorem stone_weierstrass (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc a b)) (ε : ℝ) (hε : 0 < ε) : ∃ p : Polynomial ℝ, ∀ x ∈ Set.Icc a b, |f x - p.eval x| < ε :=by
  have _ := hab
  let f_cont : C(Set.Icc a b, ℝ) := ⟨Set.restrict (Set.Icc a b) f, hf.restrict⟩
  have h_mem := continuousMap_mem_polynomialFunctions_closure a b f_cont
  change f_cont ∈ closure (polynomialFunctions (Set.Icc a b) : Set C(Set.Icc a b, ℝ)) at h_mem
  rw [Metric.mem_closure_iff] at h_mem
  rcases h_mem ε hε with ⟨g, hg, h_dist⟩
  change g ∈ polynomialFunctions (Set.Icc a b) at hg
  unfold polynomialFunctions at hg
  rw [Subalgebra.mem_map] at hg
  rcases hg with ⟨p, -, rfl⟩
  use p
  intro x hx
  have h_dist_all := (ContinuousMap.dist_lt_iff hε).mp h_dist ⟨x, hx⟩
  exact h_dist_all