a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))
rw [polynomialFunctions_closure_eq_top _ _]
no goals
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤
simp