(* Author: Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Interval Arithmetic› text ‹We provide basic interval arithmetic operations for real and complex intervals. As application we prove that complex polynomial evaluation is continuous w.r.t. interval arithmetic. To be more precise, if an interval sequence converges to some element $x$, then the interval polynomial evaluation of $f$ tends to $f(x)$.› theory Interval_Arithmetic imports Algebraic_Numbers_Prelim (* for ipoly *) begin text ‹Intervals›