Quelle  integral_cont.pvs

integral_cont[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%  Continuous functions are integrable
%
%  Author:  Rick Butler               NASA Langley
%
%------------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING


  IMPORTING integral_cont_scaf[T],
            continuous_functions

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

  in_interval  : LEMMA FORALL (PP: partition(a,b)):  
                      FORALL (ii : below(length(PP)-1)):
        (FORALL (x, y: closed_interval(seq(PP)(ii), seq(PP)(ii + 1))):
                          abs(x - y) <= seq(PP)(1 + ii) - seq(PP)(ii))

  continuous_integrable: LEMMA a < b AND    
                         (FORALL (x: closed_interval(a,b)): continuous?(f,x))
                            IMPLIES integrable?(a,b,f)


  cont_fun_integrable: COROLLARY a < b AND continuous?(f)
                                    IMPLIES integrable?(a,b,f)


END integral_cont