Real_Polynomial_Function_is_Continuous
Provedanalysiscontinuous-functionspolynomial-theoryproofwiki
A (real) polynomial function is continuous at every point. Thus a (real) polynomial function is continuous on every interval of .
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Algebra.Polynomial
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Algebra.Polynomial theorem Real_Polynomial_Function_is_Continuous (p : Polynomial ℝ) : Continuous (fun x : ℝ => Polynomial.eval x p) := by sorry
Source