Quelle  interval_minmax.pvs

interval_minmax[T: TYPE FROM real]: THEORY
%----------------------------------------------------------------------------
% 
%----------------------------------------------------------------------------
BEGIN

   ASSUMING
     IMPORTING deriv_domain_def

     connected_domain : ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING continuity_interval, reals@intervals_real

   f: VAR [T -> real]
   x,y,a,b: VAR T


   fun_cont_on(a:T,b:{x:T|a<x}): TYPE = {f | 
          (FORALL (x: closed_interval(a,b)):  
                   continuous?(restrict[T,closed_interval(a,b),real](f),x))}


   min_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
            {mx: T |  a <= mx AND mx <= b AND 
                      (FORALL (x: T): a <= x AND x <= b IMPLIES
                                      f(mx) <= f(x))}


   max_x(a:T,b:{x:T|a<x}, f: fun_cont_on(a,b)):
            {mx: T |  a <= mx AND mx <= b AND 
                      (FORALL (x: T): a <= x AND x <= b IMPLIES
                                      f(mx) >= f(x))}

END interval_minmax