continuousMap_mem_polynomialFunctions_closure

English

Equivalently, every continuous real-valued function on a compact interval is in the topological closure of polynomial functions on that interval.

Русский

Эквивалентно: любая непрерывная функция на [a,b] лежит в замыкании полиномов на этом интервале.

LaTeX

$$$f \in (\mathrm{polynomialFunctions}(\mathrm{Icc}(a,b))).\mathrm{topologicalClosure}$$$

Lean4

/-- An alternative statement of Weierstrass' theorem.

Every real-valued continuous function on `[a,b]` is a uniform limit of polynomials.
-/
theorem continuousMap_mem_polynomialFunctions_closure (a b : ℝ) (f : C(Set.Icc a b, ℝ)) :
    f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure :=
  by
  rw [polynomialFunctions_closure_eq_top _ _]
  simp

Похожие утверждения