Real_Rational_Function_is_Continuous
Provedcontinuous-functionsproofwikireal-analysis
A real rational function is continuous at every point at which it is defined. Thus a real rational function is continuous on every interval of not containing a root of the denominator of the function.
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_Rational_Function_is_Continuous (p q : Polynomial ℝ) (S : Set ℝ) (hS : ∀ x ∈ S, Polynomial.eval x q ≠ 0) : ContinuousOn (fun x : ℝ => Polynomial.eval x p / Polynomial.eval x q) S := by sorry
Source