Impressum interm_value_thm.pvs

interm_value_thm: THEORY
%-----------------------------------------------------------------
%  API for Intermediate Value Theorem
%-----------------------------------------------------------------
BEGIN

  IMPORTING continuity_interval, reals@intervals_real

  a,b,x: VAR real

  interm_value1 : LEMMA a < b IMPLIES
                              FORALL (f: [closed_interval(a,b) -> real]):
                              continuous?(f) AND f(a) < x AND x < f(b)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_value2 : LEMMA a < b IMPLIES
                              FORALL (f: [closed_interval(a,b) -> real]):
                              continuous?(f) AND f(a) <= x AND x <= f(b)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_value3 : LEMMA a < b IMPLIES
                              FORALL (f: [closed_interval(a,b) -> real]):
                              continuous?(f) AND f(b) < x AND x < f(a)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_value4 : LEMMA a < b IMPLIES
                              FORALL (f: [closed_interval(a,b) -> real]):
                              continuous?(f) AND f(b) <= x AND x <= f(a)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_value5 : LEMMA a < b IMPLIES
                              FORALL (f: [closed_interval(a,b) -> real],p,q:closed_interval(a,b)):
                              continuous?(f) AND f(p) <= x AND x <= f(q)
                         IMPLIES EXISTS (c: closed_interval(a,b)): 
    ((p<=c AND c<=q) OR (q<=c AND c<=p)) AND f(c) = x


  f: VAR [real -> real]


  cont_intv : LEMMA a < b AND continuous?(f) 
              IMPLIES continuous?(LAMBDA (x: closed_interval(a, b)): f(x))


  cont_intv1: LEMMA a < b AND continuous?[closed_interval[real](a, b)](f) 
              IMPLIES continuous?(LAMBDA (x: closed_interval(a, b)): f(x))




  interm_val1 : LEMMA a < b IMPLIES
                              continuous?[closed_interval(a,b)](f) AND f(a) < x AND x < f(b)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_val2 : LEMMA a < b IMPLIES
                              FORALL (f: [real -> real]):
                              continuous?[closed_interval(a,b)](f) AND f(a) <= x AND x <= f(b)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_val3 : LEMMA a < b IMPLIES
                              FORALL (f: [real -> real]):
                              continuous?[closed_interval(a,b)](f) AND f(b) < x AND x < f(a)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  interm_val4 : LEMMA a < b IMPLIES
                              FORALL (f: [real -> real]):
                              continuous?[closed_interval(a,b)](f) AND f(b) <= x AND x <= f(a)
                         IMPLIES EXISTS (c: closed_interval(a,b)): f(c) = x

  % ----------------------------------------------------------------------------------

  xl,xu: VAR real

  zeros_interm: LEMMA  continuous?(f)
                     AND f(xl) = 0 AND f(xu) = 0 AND
                    (FORALL (x: open_interval(xl,xu)): f(x) /= 0)
                  IMPLIES
                    (FORALL (x: open_interval(xl,xu)): f(x) > 0) OR
                    (FORALL (x: open_interval(xl,xu)): f(x) < 0)

  % ----------------------------------------------------------------------------------

  IMPORTING reals@connected_set

  ab : VAR Connected

  IntermediateValue : THEOREM
    FORALL (f:[real->real]):
    continuous?(f) AND
    (FORALL (c:(ab)) : f(c) /= 0) IMPLIES 
    (FORALL (x,y:(ab)) : f(x)*f(y) > 0)       

END interm_value_thm