Quelle  rs_integral_cont.pvs

rs_integral_cont[T:TYPE+ from real]: THEORY
%------------------------------------------------------------------------------
%  Continuous functions are Riemann-Stieltjes integrable
%------------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def[T]

      connected_domain : ASSUMPTION connected?[T]


      not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING


  IMPORTING real_metric_space,
     uniform_continuity,
     rs_integral_prep[T],
     bounded_variation[T]

   a,b,x,y,z: VAR T
   c,S: VAR real
   D,m,M,v1,v2,cc,RS1,RS2,K: VAR real
   delta : VAR posreal

   f,g,h,G: VAR [T -> real]


  RS_integrable_cont_inc: LEMMA a < b IMPLIES
      LET CI = closed_intv[T](a,b) IN
                         (continuous?[T,real_dist,real,real_dist](f,closed_intv[T](a,b)) AND
    increasing?[(CI)](g)
                         IMPLIES integrable?(a,b,g,f))

  RS_integrable_cont_BV: LEMMA a < b IMPLIES
      LET CI = closed_intv[T](a,b) IN
                         (continuous?[T,real_dist,real,real_dist](f,closed_intv[T](a,b)) AND
    bounded_variation?(a,b)(g)
                         IMPLIES integrable?(a,b,g,f)) 





END rs_integral_cont